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?