How to avoid awkward assertions

Using Coq
1

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?

2

How about rewrite Nat.sub_0_r? :slight_smile:

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?

3

Thanks for your sincere help!

I am just learning by myself.