Let b0 be given.
Assume Hb0Sq: b0 ∈ ordered_square.
Assume Hp10b0: order_rel (setprod R R) ordsq_p10 b0.
Set p10 to be the term ordsq_p10.
Set w to be the term (add_SNo 1 (minus_SNo (inv_nat 1)),eps_ 1).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H1not0: 1 ∉ {0}.
Assume H10: 1 ∈ {0}.
We prove the intermediate claim Heq: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H10).
An exact proof term for the current goal is (neq_1_0 Heq).
We prove the intermediate claim H1In: 1 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} 1 H1omega H1not0).
We prove the intermediate claim HwB: w ∈ ordsq_B.
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) 1 H1In).
We prove the intermediate claim HwSq: w ∈ ordered_square.
An exact proof term for the current goal is (ordsq_B_sub_ordered_square w HwB).
We prove the intermediate claim Hp10def: p10 = (1,0).
Use reflexivity.
We prove the intermediate claim Hp10Sq: p10 ∈ ordered_square.
rewrite the current goal using Hp10def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval 1 0 one_in_unit_interval zero_in_unit_interval).
We prove the intermediate claim HwRR: w ∈ setprod R R.
An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) w HwSq).
We prove the intermediate claim Hp10RR: p10 ∈ setprod R R.
An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) p10 Hp10Sq).
We prove the intermediate claim Hb0RR: b0 ∈ setprod R R.
An exact proof term for the current goal is ((setprod_Subq unit_interval unit_interval R R unit_interval_sub_R unit_interval_sub_R) b0 Hb0Sq).
We prove the intermediate claim Hw0: add_SNo 1 (minus_SNo (inv_nat 1)) = 0.
We prove the intermediate claim Hinv1eq: inv_nat 1 = 1.
We will prove inv_nat 1 = 1.
We prove the intermediate claim H1neq0': 1 ≠ 0.
An exact proof term for the current goal is neq_1_0.
We prove the intermediate claim Hmul: mul_SNo 1 (inv_nat 1) = 1.
An exact proof term for the current goal is (recip_SNo_invR 1 SNo_1 H1neq0').
rewrite the current goal using (mul_SNo_oneL (inv_nat 1) (SNo_recip_SNo 1 SNo_1)) (from right to left) at position 1.
An exact proof term for the current goal is Hmul.
rewrite the current goal using Hinv1eq (from left to right).
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv 1 SNo_1).
We prove the intermediate claim Hweq: w = (0,eps_ 1).
rewrite the current goal using Hw0 (from left to right).
Use reflexivity.
We prove the intermediate claim Hwp10: order_rel (setprod R R) w p10.
rewrite the current goal using Hweq (from left to right).
rewrite the current goal using Hp10def (from left to right).
Apply (order_rel_setprod_R_R_intro 0 (eps_ 1) 1 0) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Rlt_0_1.
We prove the intermediate claim Hwb0: order_rel (setprod R R) w b0.
An exact proof term for the current goal is (order_rel_trans (setprod R R) w p10 b0 simply_ordered_set_setprod_R_R HwRR Hp10RR Hb0RR Hwp10 Hp10b0).
We use w to witness the existential quantifier.
Apply andI to the current goal.
Apply (SepI ordered_square (λx0 : set ⇒ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
An exact proof term for the current goal is Hwb0.
An exact proof term for the current goal is HwB.
∎