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?