Let n and m be given.
Assume Hn: n ∈ ω.
Assume Hm: m ∈ ω.
Assume Heq: apply_fun seq_one_over_n n = apply_fun seq_one_over_n m.
We will prove n = m.
We prove the intermediate claim HnEq: apply_fun seq_one_over_n n = inv_nat (ordsucc n).
An exact proof term for the current goal is (seq_one_over_n_apply n Hn).
We prove the intermediate claim HmEq: apply_fun seq_one_over_n m = inv_nat (ordsucc m).
An exact proof term for the current goal is (seq_one_over_n_apply m Hm).
We prove the intermediate claim Heq': inv_nat (ordsucc n) = inv_nat (ordsucc m).
We will prove inv_nat (ordsucc n) = inv_nat (ordsucc m).
rewrite the current goal using HnEq (from right to left).
rewrite the current goal using HmEq (from right to left).
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (inv_nat_ordsucc_inj n m Hn Hm Heq').
∎