Let w be given.
Assume HwB: w ∈ ordsq_B.
We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, w = (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) w HwB).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
Apply Hnpack to the current goal.
Assume HnIn HwEq.
rewrite the current goal using HwEq (from left to right).
Set inv to be the term inv_nat n.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
We prove the intermediate claim HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos n HnIn).
We prove the intermediate claim HinvPos: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPosR).
We prove the intermediate claim H10eq: add_SNo 1 0 = 1.
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H1lt: 1 < add_SNo 1 inv.
We prove the intermediate claim Htmp: add_SNo 1 0 < add_SNo 1 inv.
An exact proof term for the current goal is (add_SNo_Lt2 1 0 inv SNo_1 SNo_0 HinvS HinvPos).
rewrite the current goal using H10eq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hxlt: add_SNo 1 (minus_SNo inv) < 1.
An exact proof term for the current goal is (add_SNo_minus_Lt1b 1 inv 1 SNo_1 HinvS SNo_1 H1lt).
We prove the intermediate claim HxR: add_SNo 1 (minus_SNo inv) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo inv) (real_minus_SNo inv HinvR)).
We prove the intermediate claim HxltR: Rlt (add_SNo 1 (minus_SNo inv)) 1.
An exact proof term for the current goal is (RltI (add_SNo 1 (minus_SNo inv)) 1 HxR real_1 Hxlt).
We prove the intermediate claim Hp10def: ordsq_p10 = (1,0).
Use reflexivity.
rewrite the current goal using Hp10def (from left to right).
Apply (order_rel_setprod_R_R_intro (add_SNo 1 (minus_SNo inv)) (eps_ 1) 1 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is HxltR.
∎