Let n and m be given.
Assume Hn: n ∈ ω.
Assume Hm: m ∈ ω.
Assume Heq: inv_nat (ordsucc n) = inv_nat (ordsucc m).
We will prove n = m.
We prove the intermediate claim Hn_ord: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n Hn).
We prove the intermediate claim Hm_ord: ordinal m.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal m Hm).
We prove the intermediate claim Hposn: 0 < ordsucc n.
An exact proof term for the current goal is (ordinal_ordsucc_pos n Hn_ord).
We prove the intermediate claim Hposm: 0 < ordsucc m.
An exact proof term for the current goal is (ordinal_ordsucc_pos m Hm_ord).
We prove the intermediate claim Hn1: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n Hn).
We prove the intermediate claim Hm1: ordsucc m ∈ ω.
An exact proof term for the current goal is (omega_ordsucc m Hm).
We prove the intermediate claim HSn: SNo (ordsucc n).
An exact proof term for the current goal is (omega_SNo (ordsucc n) Hn1).
We prove the intermediate claim HSm: SNo (ordsucc m).
An exact proof term for the current goal is (omega_SNo (ordsucc m) Hm1).
We prove the intermediate claim Hposcase_n: inv_nat (ordsucc n) = recip_SNo_pos (ordsucc n).
An exact proof term for the current goal is (recip_SNo_poscase (ordsucc n) Hposn).
We prove the intermediate claim Hposcase_m: inv_nat (ordsucc m) = recip_SNo_pos (ordsucc m).
An exact proof term for the current goal is (recip_SNo_poscase (ordsucc m) Hposm).
We prove the intermediate claim Hpos_eq: recip_SNo_pos (ordsucc n) = recip_SNo_pos (ordsucc m).
We will prove recip_SNo_pos (ordsucc n) = recip_SNo_pos (ordsucc m).
rewrite the current goal using Hposcase_n (from right to left).
rewrite the current goal using Hposcase_m (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hinv_eq: recip_SNo_pos (recip_SNo_pos (ordsucc n)) = recip_SNo_pos (recip_SNo_pos (ordsucc m)).
We will prove recip_SNo_pos (recip_SNo_pos (ordsucc n)) = recip_SNo_pos (recip_SNo_pos (ordsucc m)).
rewrite the current goal using Hpos_eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hord: ordsucc n = ordsucc m.
We will prove ordsucc n = ordsucc m.
rewrite the current goal using (recip_SNo_pos_invol (ordsucc n) HSn Hposn) (from right to left).
rewrite the current goal using (recip_SNo_pos_invol (ordsucc m) HSm Hposm) (from right to left).
An exact proof term for the current goal is Hinv_eq.
An exact proof term for the current goal is (ordsucc_inj n m Hord).
∎