Let a0 and b0 be given.
Assume Ha0Sq: a0 ∈ ordered_square.
Assume Hb0Sq: b0 ∈ ordered_square.
Assume Ha0p10: order_rel (setprod R R) a0 ordsq_p10.
Assume Hp10b0: order_rel (setprod R R) ordsq_p10 b0.
Set p10 to be the term ordsq_p10.
We prove the intermediate claim Hp10def: p10 = (1,0).
Use reflexivity.
We prove the intermediate claim Ha0xU: a0 0 ∈ unit_interval.
An exact proof term for the current goal is (ap0_Sigma unit_interval (λ_ : set ⇒ unit_interval) a0 Ha0Sq).
We prove the intermediate claim Ha0yU: a0 1 ∈ unit_interval.
An exact proof term for the current goal is (ap1_Sigma unit_interval (λ_ : set ⇒ unit_interval) a0 Ha0Sq).
We prove the intermediate claim Ha0yprop: ¬ (Rlt (a0 1) 0) ∧ ¬ (Rlt 1 (a0 1)).
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) (a0 1) Ha0yU).
We prove the intermediate claim Ha0ynlt0: ¬ (Rlt (a0 1) 0).
An exact proof term for the current goal is (andEL (¬ (Rlt (a0 1) 0)) (¬ (Rlt 1 (a0 1))) Ha0yprop).
We prove the intermediate claim Hunf: ∃a1 a2 b1 b2 : set, a0 = (a1,a2) ∧ p10 = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
An exact proof term for the current goal is (order_rel_setprod_R_R_unfold a0 p10 Ha0p10).
Apply Hunf to the current goal.
Let a1 be given.
Assume H1.
Apply H1 to the current goal.
Let a2 be given.
Assume H2.
Apply H2 to the current goal.
Let b1 be given.
Assume H3.
Apply H3 to the current goal.
Let b2 be given.
Assume Hconj.
Apply Hconj to the current goal.
Assume Hcore Hdisj.
Apply Hcore to the current goal.
Assume Ha0eq Hp10eq.
We prove the intermediate claim Ha0_0_eq: a0 0 = a1.
rewrite the current goal using Ha0eq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq a1 a2).
We prove the intermediate claim Ha0_1_eq: a0 1 = a2.
rewrite the current goal using Ha0eq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq a1 a2).
We prove the intermediate claim Heqp: (1,0) = (b1,b2).
rewrite the current goal using Hp10def (from right to left) at position 1.
rewrite the current goal using Hp10eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hb1eq: b1 = 1.
We prove the intermediate claim H0eq: (1,0) 0 = (b1,b2) 0.
rewrite the current goal using Heqp (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp: 1 = b1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left).
rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).
An exact proof term for the current goal is H0eq.
rewrite the current goal using Htmp (from right to left).
Use reflexivity.
We prove the intermediate claim Hb2eq: b2 = 0.
We prove the intermediate claim H1eq: (1,0) 1 = (b1,b2) 1.
rewrite the current goal using Heqp (from left to right).
Use reflexivity.
We prove the intermediate claim Htmp: 0 = b2.
rewrite the current goal using (tuple_2_1_eq 1 0) (from right to left).
rewrite the current goal using (tuple_2_1_eq b1 b2) (from right to left).
An exact proof term for the current goal is H1eq.
rewrite the current goal using Htmp (from right to left).
Use reflexivity.
We prove the intermediate claim Ha1U: a1 ∈ unit_interval.
rewrite the current goal using Ha0_0_eq (from right to left) at position 1.
An exact proof term for the current goal is Ha0xU.
We prove the intermediate claim Ha1R: a1 ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x)) a1 Ha1U).
We prove the intermediate claim Ha1S: SNo a1.
An exact proof term for the current goal is (real_SNo a1 Ha1R).
We prove the intermediate claim Ha1lt1: Rlt a1 1.
We will prove Rlt a1 1.
Apply Hdisj to the current goal.
Assume Hlt: Rlt a1 b1.
rewrite the current goal using Hb1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Assume Heqand: a1 = b1 ∧ Rlt a2 b2.
Apply FalseE to the current goal.
We prove the intermediate claim Ha2lt: Rlt a2 b2.
An exact proof term for the current goal is (andER (a1 = b1) (Rlt a2 b2) Heqand).
We prove the intermediate claim Ha2lt0: Rlt a2 0.
rewrite the current goal using Hb2eq (from right to left) at position 1.
An exact proof term for the current goal is Ha2lt.
We prove the intermediate claim Ha0ylt0: Rlt (a0 1) 0.
rewrite the current goal using Ha0_1_eq (from left to right) at position 1.
An exact proof term for the current goal is Ha2lt0.
An exact proof term for the current goal is (Ha0ynlt0 Ha0ylt0).
Set diff to be the term add_SNo 1 (minus_SNo a1).
We prove the intermediate claim HdiffR: diff ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo a1) (real_minus_SNo a1 Ha1R)).
We prove the intermediate claim Hdiffpos: Rlt 0 diff.
An exact proof term for the current goal is (Rlt_0_diff_of_lt a1 1 Ha1lt1).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) diff.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt_local diff HdiffR Hdiffpos).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
Apply HNpack to the current goal.
Assume HNO HinvLtR.
Set n to be the term ordsucc N.
We prove the intermediate claim Hndef: n = ordsucc N.
Use reflexivity.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNO).
We prove the intermediate claim Hnnot0: n ∉ {0}.
Assume Hn0: n ∈ {0}.
We prove the intermediate claim Heq0: n = 0.
An exact proof term for the current goal is (SingE 0 n Hn0).
We prove the intermediate claim Heq1: ordsucc N = 0.
rewrite the current goal using Hndef (from right to left) at position 1.
An exact proof term for the current goal is Heq0.
An exact proof term for the current goal is ((neq_ordsucc_0 N) Heq1).
We prove the intermediate claim HnIn: n ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} n HnO Hnnot0).
Set w to be the term (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).
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)) n HnIn).
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 HinvLtS: inv_nat n < diff.
An exact proof term for the current goal is (RltE_lt (inv_nat n) diff HinvLtR).
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
We prove the intermediate claim HinvS: SNo (inv_nat n).
An exact proof term for the current goal is (real_SNo (inv_nat n) HinvR).
We prove the intermediate claim HsumLt: add_SNo (inv_nat n) a1 < 1.
An exact proof term for the current goal is (add_SNo_minus_Lt2 1 a1 (inv_nat n) SNo_1 Ha1S HinvS HinvLtS).
We prove the intermediate claim Hcom: add_SNo (inv_nat n) a1 = add_SNo a1 (inv_nat n).
An exact proof term for the current goal is (add_SNo_com (inv_nat n) a1 HinvS Ha1S).
We prove the intermediate claim HsumLt2: add_SNo a1 (inv_nat n) < 1.
rewrite the current goal using Hcom (from right to left) at position 1.
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim Ha1ltwx: a1 < add_SNo 1 (minus_SNo (inv_nat n)).
An exact proof term for the current goal is (add_SNo_minus_Lt2b 1 (inv_nat n) a1 SNo_1 HinvS Ha1S HsumLt2).
We prove the intermediate claim HwxR: add_SNo 1 (minus_SNo (inv_nat n)) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo (inv_nat n)) (real_minus_SNo (inv_nat n) HinvR)).
We prove the intermediate claim Ha1ltwxR: Rlt a1 (add_SNo 1 (minus_SNo (inv_nat n))).
An exact proof term for the current goal is (RltI a1 (add_SNo 1 (minus_SNo (inv_nat n))) Ha1R HwxR Ha1ltwx).
We prove the intermediate claim Ha0w: order_rel (setprod R R) a0 w.
rewrite the current goal using Ha0eq (from left to right).
Apply (order_rel_setprod_R_R_intro a1 a2 (add_SNo 1 (minus_SNo (inv_nat n))) (eps_ 1)) to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is Ha1ltwxR.
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 Hwp10: order_rel (setprod R R) w p10.
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).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).
Set inv to be the term inv_nat n.
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).
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.
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) a0 x0 ∧ order_rel (setprod R R) x0 b0) w HwSq) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0w.
An exact proof term for the current goal is Hwb0.
An exact proof term for the current goal is HwB.
∎