# How to avoid awkward assertions

**URL:** <https://discourse.rocq-prover.org/t/how-to-avoid-awkward-assertions/1153>\
**Category:** Using Rocq\
**Created:** [December 11, 2020, 7:36pm UTC](https://discourse.rocq-prover.org/t/how-to-avoid-awkward-assertions/1153 "2020-12-11T19:36:45Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![ZWY](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zwy/32/335_2.png) [@ZWY](https://discourse.rocq-prover.org/u/ZWY)\
**Post date:** [December 11, 2020, 7:36pm UTC](https://discourse.rocq-prover.org/t/how-to-avoid-awkward-assertions/1153/1 "2020-12-11T19:36:45Z")

</div>

For a proof state

```
l : list nat
x, m : nat
H0 : 1 <= m
______________________________________ (1/1)
nth (m - 0) l 0 = nth m l 0

```

we can rely on `Nat.sub_0_r: forall n : nat, n - 0 = n` to prove it.  
However, I only know we can first run `assert (I1: m - 0 = m)` and then use the assertion I1 `rewrite I1. reflexivity.` to construct a proof.

I think the assertion is rather awkward and want to avoid such usages. Could you give me some help?

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [December 11, 2020, 8:21pm UTC](https://discourse.rocq-prover.org/t/how-to-avoid-awkward-assertions/1153/2 "2020-12-11T20:21:43Z")

</div>

How about `rewrite Nat.sub_0_r`? 🙂

Maybe more importantly: What’s your reference for learning Coq? Is this part of a course (I think the question was perfectly fine, so it’s no problem if it was from a course) or are you learning Coq on your own?

---

<div class="post-metadata">

**Author:** ![ZWY](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zwy/32/335_2.png) [@ZWY](https://discourse.rocq-prover.org/u/ZWY)\
**Post date:** [December 11, 2020, 8:46pm UTC](https://discourse.rocq-prover.org/t/how-to-avoid-awkward-assertions/1153/3 "2020-12-11T20:46:42Z")

</div>

Thanks for your sincere help!

I am just learning by myself.