We will prove Rlt (inv_nat 2) 1.
We prove the intermediate claim H0o: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H1o: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is In_0_1.
We prove the intermediate claim Hlt: Rlt (inv_nat (ordsucc 1)) (inv_nat (ordsucc 0)).
An exact proof term for the current goal is (inv_nat_ordsucc_antitone 0 1 H0o H1o H0in1).
We prove the intermediate claim Hs0: ordsucc 0 = 1.
We prove the intermediate claim Heq: add_SNo 0 1 = ordsucc 0.
An exact proof term for the current goal is (add_SNo_1_ordsucc 0 H0o).
We prove the intermediate claim Heq01: add_SNo 0 1 = 1.
An exact proof term for the current goal is (add_SNo_0L 1 SNo_1).
We will prove ordsucc 0 = 1.
rewrite the current goal using Heq (from right to left).
rewrite the current goal using Heq01 (from left to right).
Use reflexivity.
We prove the intermediate claim Hs1: ordsucc 1 = 2.
We prove the intermediate claim Heq: add_SNo 1 1 = ordsucc 1.
An exact proof term for the current goal is (add_SNo_1_ordsucc 1 H1o).
We will prove ordsucc 1 = 2.
rewrite the current goal using Heq (from right to left).
rewrite the current goal using add_SNo_1_1_2 (from left to right).
Use reflexivity.
rewrite the current goal using inv_nat_1_eq_1 (from right to left) at position 2.
rewrite the current goal using Hs1 (from right to left) at position 1.
rewrite the current goal using Hs0 (from right to left) at position 2.
An exact proof term for the current goal is Hlt.
∎