Let X, a and b be given.
Assume Hso HaX HbX.
Let p be given.
Assume Habp Heqp Hbap.
Apply (xm (X = R)) to the current goal.
Assume HX: X = R.
We prove the intermediate claim HaR: a ∈ R.
rewrite the current goal using HX (from right to left).
An exact proof term for the current goal is HaX.
We prove the intermediate claim HbR: b ∈ R.
rewrite the current goal using HX (from right to left).
An exact proof term for the current goal is HbX.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
Apply (SNoLt_trichotomy_or_impred a b HaS HbS p) to the current goal.
Assume Hablt: a < b.
We prove the intermediate claim HabRlt: Rlt a b.
An exact proof term for the current goal is (RltI a b HaR HbR Hablt).
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HX (from left to right).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a b HabRlt).
An exact proof term for the current goal is (Habp Hrel).
Assume Heq: a = b.
An exact proof term for the current goal is (Heqp Heq).
Assume Hbalt: b < a.
We prove the intermediate claim HbaRlt: Rlt b a.
An exact proof term for the current goal is (RltI b a HbR HaR Hbalt).
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HX (from left to right).
An exact proof term for the current goal is (Rlt_implies_order_rel_R b a HbaRlt).
An exact proof term for the current goal is (Hbap Hrel).
Assume HneqR: ¬ (X = R).
Apply (xm (X = rational_numbers)) to the current goal.
Assume HXQ: X = rational_numbers.
We prove the intermediate claim HaQ: a ∈ rational_numbers.
rewrite the current goal using HXQ (from right to left).
An exact proof term for the current goal is HaX.
We prove the intermediate claim HbQ: b ∈ rational_numbers.
rewrite the current goal using HXQ (from right to left).
An exact proof term for the current goal is HbX.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R a HaQ).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R b HbQ).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
Apply (SNoLt_trichotomy_or_impred a b HaS HbS p) to the current goal.
Assume Hablt: a < b.
We prove the intermediate claim HabRlt: Rlt a b.
An exact proof term for the current goal is (RltI a b HaR HbR Hablt).
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HXQ (from left to right).
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a b HabRlt).
An exact proof term for the current goal is (Habp Hrel).
Assume Heq: a = b.
An exact proof term for the current goal is (Heqp Heq).
Assume Hbalt: b < a.
We prove the intermediate claim HbaRlt: Rlt b a.
An exact proof term for the current goal is (RltI b a HbR HaR Hbalt).
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HXQ (from left to right).
An exact proof term for the current goal is (Rlt_implies_order_rel_Q b a HbaRlt).
An exact proof term for the current goal is (Hbap Hrel).
Assume HneqQ: ¬ (X = rational_numbers).
Apply (xm (X = ω)) to the current goal.
Assume HXo: X = ω.
We prove the intermediate claim HaO: a ∈ ω.
rewrite the current goal using HXo (from right to left).
An exact proof term for the current goal is HaX.
We prove the intermediate claim HbO: b ∈ ω.
rewrite the current goal using HXo (from right to left).
An exact proof term for the current goal is HbX.
We prove the intermediate claim HaOrd: ordinal a.
An exact proof term for the current goal is (nat_p_ordinal a (omega_nat_p a HaO)).
We prove the intermediate claim HbOrd: ordinal b.
An exact proof term for the current goal is (nat_p_ordinal b (omega_nat_p b HbO)).
Apply (ordinal_trichotomy_or_impred a b HaOrd HbOrd p) to the current goal.
Assume Habmem: a ∈ b.
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HXo (from left to right).
An exact proof term for the current goal is (mem_implies_order_rel_omega a b Habmem).
An exact proof term for the current goal is (Habp Hrel).
Assume Heq: a = b.
An exact proof term for the current goal is (Heqp Heq).
Assume Hbmem: b ∈ a.
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HXo (from left to right).
An exact proof term for the current goal is (mem_implies_order_rel_omega b a Hbmem).
An exact proof term for the current goal is (Hbap Hrel).
Assume HneqO: ¬ (X = ω).
Apply (xm (X = ω ∖ {0})) to the current goal.
Assume HXnz: X = ω ∖ {0}.
We prove the intermediate claim HaNz: a ∈ ω ∖ {0}.
rewrite the current goal using HXnz (from right to left).
An exact proof term for the current goal is HaX.
We prove the intermediate claim HbNz: b ∈ ω ∖ {0}.
rewrite the current goal using HXnz (from right to left).
An exact proof term for the current goal is HbX.
We prove the intermediate claim HaO: a ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} a HaNz).
We prove the intermediate claim HbO: b ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} b HbNz).
We prove the intermediate claim HaOrd: ordinal a.
An exact proof term for the current goal is (nat_p_ordinal a (omega_nat_p a HaO)).
We prove the intermediate claim HbOrd: ordinal b.
An exact proof term for the current goal is (nat_p_ordinal b (omega_nat_p b HbO)).
Apply (ordinal_trichotomy_or_impred a b HaOrd HbOrd p) to the current goal.
Assume Habmem: a ∈ b.
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HXnz (from left to right).
An exact proof term for the current goal is (mem_implies_order_rel_omega_nonzero a b Habmem).
An exact proof term for the current goal is (Habp Hrel).
Assume Heq: a = b.
An exact proof term for the current goal is (Heqp Heq).
Assume Hbmem: b ∈ a.
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HXnz (from left to right).
An exact proof term for the current goal is (mem_implies_order_rel_omega_nonzero b a Hbmem).
An exact proof term for the current goal is (Hbap Hrel).
Assume HneqNz: ¬ (X = ω ∖ {0}).
Apply (xm (X = setprod 2 ω)) to the current goal.
Assume HX2: X = setprod 2 ω.
We prove the intermediate claim HaP: a ∈ setprod 2 ω.
rewrite the current goal using HX2 (from right to left).
An exact proof term for the current goal is HaX.
We prove the intermediate claim HbP: b ∈ setprod 2 ω.
rewrite the current goal using HX2 (from right to left).
An exact proof term for the current goal is HbX.
Apply (Sigma_E 2 (λ_ : set ⇒ ω) a HaP) to the current goal.
Let i be given.
Assume Ha1.
Apply Ha1 to the current goal.
Assume Hi2 Ha2.
Apply Ha2 to the current goal.
Let m be given.
Assume Ha3.
Apply Ha3 to the current goal.
Assume HmO HaEqPair.
Apply (Sigma_E 2 (λ_ : set ⇒ ω) b HbP) to the current goal.
Let j be given.
Assume Hb1.
Apply Hb1 to the current goal.
Assume Hj2 Hb2.
Apply Hb2 to the current goal.
Let n be given.
Assume Hb3.
Apply Hb3 to the current goal.
Assume HnO HbEqPair.
We prove the intermediate claim HaEq: a = (i,m).
rewrite the current goal using HaEqPair (from left to right).
An exact proof term for the current goal is (tuple_pair i m).
We prove the intermediate claim HbEq: b = (j,n).
rewrite the current goal using HbEqPair (from left to right).
An exact proof term for the current goal is (tuple_pair j n).
We prove the intermediate claim H2ord: ordinal 2.
An exact proof term for the current goal is (nat_p_ordinal 2 nat_2).
We prove the intermediate claim HiOrd: ordinal i.
An exact proof term for the current goal is (ordinal_Hered 2 H2ord i Hi2).
We prove the intermediate claim HjOrd: ordinal j.
An exact proof term for the current goal is (ordinal_Hered 2 H2ord j Hj2).
We prove the intermediate claim HmOrd: ordinal m.
An exact proof term for the current goal is (nat_p_ordinal m (omega_nat_p m HmO)).
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (nat_p_ordinal n (omega_nat_p n HnO)).
Apply (ordinal_trichotomy_or_impred i j HiOrd HjOrd p) to the current goal.
Assume Hijmem: i ∈ j.
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HX2 (from left to right).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_intro i m j n Hi2 HmO Hj2 HnO (orIL (i ∈ j) (i = j ∧ m ∈ n) Hijmem)).
An exact proof term for the current goal is (Habp Hrel).
Assume Hijeq: i = j.
Apply (ordinal_trichotomy_or_impred m n HmOrd HnOrd p) to the current goal.
Assume Hmnmem: m ∈ n.
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HX2 (from left to right).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_intro i m j n Hi2 HmO Hj2 HnO (orIR (i ∈ j) (i = j ∧ m ∈ n) (andI (i = j) (m ∈ n) Hijeq Hmnmem))).
An exact proof term for the current goal is (Habp Hrel).
Assume Hmneq: m = n.
We prove the intermediate claim HabEq: a = b.
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (coords_eq_tuple i m j n Hijeq Hmneq).
An exact proof term for the current goal is (Heqp HabEq).
Assume Hnmemb: n ∈ m.
We prove the intermediate claim Hji: j = i.
Use symmetry.
An exact proof term for the current goal is Hijeq.
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HX2 (from left to right).
rewrite the current goal using HbEq (from left to right).
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_intro j n i m Hj2 HnO Hi2 HmO (orIR (j ∈ i) (j = i ∧ n ∈ m) (andI (j = i) (n ∈ m) Hji Hnmemb))).
An exact proof term for the current goal is (Hbap Hrel).
Assume Hjimmem: j ∈ i.
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HX2 (from left to right).
rewrite the current goal using HbEq (from left to right).
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_intro j n i m Hj2 HnO Hi2 HmO (orIL (j ∈ i) (j = i ∧ n ∈ m) Hjimmem)).
An exact proof term for the current goal is (Hbap Hrel).
Assume Hneq2: ¬ (X = setprod 2 ω).
Apply (xm (X = setprod R R)) to the current goal.
Assume HXR2: X = setprod R R.
We prove the intermediate claim HaP: a ∈ setprod R R.
rewrite the current goal using HXR2 (from right to left).
An exact proof term for the current goal is HaX.
We prove the intermediate claim HbP: b ∈ setprod R R.
rewrite the current goal using HXR2 (from right to left).
An exact proof term for the current goal is HbX.
Apply (Sigma_E R (λ_ : set ⇒ R) a HaP) to the current goal.
Let a1 be given.
Assume Ha1.
Apply Ha1 to the current goal.
Assume Ha1R Ha2.
Apply Ha2 to the current goal.
Let a2 be given.
Assume Ha3.
Apply Ha3 to the current goal.
Assume Ha2R HaEqPair.
Apply (Sigma_E R (λ_ : set ⇒ R) b HbP) to the current goal.
Let b1 be given.
Assume Hb1.
Apply Hb1 to the current goal.
Assume Hb1R Hb2.
Apply Hb2 to the current goal.
Let b2 be given.
Assume Hb3.
Apply Hb3 to the current goal.
Assume Hb2R HbEqPair.
We prove the intermediate claim HaEq: a = (a1,a2).
rewrite the current goal using HaEqPair (from left to right).
An exact proof term for the current goal is (tuple_pair a1 a2).
We prove the intermediate claim HbEq: b = (b1,b2).
rewrite the current goal using HbEqPair (from left to right).
An exact proof term for the current goal is (tuple_pair b1 b2).
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 Hb1S: SNo b1.
An exact proof term for the current goal is (real_SNo b1 Hb1R).
We prove the intermediate claim Ha2S: SNo a2.
An exact proof term for the current goal is (real_SNo a2 Ha2R).
We prove the intermediate claim Hb2S: SNo b2.
An exact proof term for the current goal is (real_SNo b2 Hb2R).
Apply (SNoLt_trichotomy_or_impred a1 b1 Ha1S Hb1S p) to the current goal.
Assume Hab1: a1 < b1.
We prove the intermediate claim HabRlt: Rlt a1 b1.
An exact proof term for the current goal is (RltI a1 b1 Ha1R Hb1R Hab1).
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HXR2 (from left to right).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
We will prove order_rel (setprod R R) (a1,a2) (b1,b2).
We will prove (setprod R R = R ∧ Rlt (a1,a2) (b1,b2)) ∨ (setprod R R = rational_numbers ∧ Rlt (a1,a2) (b1,b2)) ∨ (setprod R R = ω ∧ (a1,a2) ∈ (b1,b2)) ∨ (setprod R R = ω ∖ {0} ∧ (a1,a2) ∈ (b1,b2)) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (a1,a2) = (i,m) ∧ (b1,b2) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ (a1,a2) ∈ (b1,b2)).
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
Apply andI to the current goal.
Use reflexivity.
We use a1 to witness the existential quantifier.
We use a2 to witness the existential quantifier.
We use b1 to witness the existential quantifier.
We use b2 to witness the existential quantifier.
Apply and3I to the current goal.
Use reflexivity.
Use reflexivity.
An exact proof term for the current goal is (orIL (Rlt a1 b1) (a1 = b1 ∧ Rlt a2 b2) HabRlt).
An exact proof term for the current goal is (Habp Hrel).
Assume H1eq: a1 = b1.
Apply (SNoLt_trichotomy_or_impred a2 b2 Ha2S Hb2S p) to the current goal.
Assume Hab2: a2 < b2.
We prove the intermediate claim HabRlt: Rlt a2 b2.
An exact proof term for the current goal is (RltI a2 b2 Ha2R Hb2R Hab2).
We prove the intermediate claim Hrel: order_rel X a b.
rewrite the current goal using HXR2 (from left to right).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
We will prove order_rel (setprod R R) (a1,a2) (b1,b2).
We will prove (setprod R R = R ∧ Rlt (a1,a2) (b1,b2)) ∨ (setprod R R = rational_numbers ∧ Rlt (a1,a2) (b1,b2)) ∨ (setprod R R = ω ∧ (a1,a2) ∈ (b1,b2)) ∨ (setprod R R = ω ∖ {0} ∧ (a1,a2) ∈ (b1,b2)) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (a1,a2) = (i,m) ∧ (b1,b2) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ (a1,a2) ∈ (b1,b2)).
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
Apply andI to the current goal.
Use reflexivity.
We use a1 to witness the existential quantifier.
We use a2 to witness the existential quantifier.
We use b1 to witness the existential quantifier.
We use b2 to witness the existential quantifier.
Apply and3I to the current goal.
Use reflexivity.
Use reflexivity.
An exact proof term for the current goal is (orIR (Rlt a1 b1) (a1 = b1 ∧ Rlt a2 b2) (andI (a1 = b1) (Rlt a2 b2) H1eq HabRlt)).
An exact proof term for the current goal is (Habp Hrel).
Assume HabEq: a2 = b2.
We prove the intermediate claim HabEq2: a = b.
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (coords_eq_tuple a1 a2 b1 b2 H1eq HabEq).
An exact proof term for the current goal is (Heqp HabEq2).
Assume Hba2: b2 < a2.
We prove the intermediate claim HbaRlt: Rlt b2 a2.
An exact proof term for the current goal is (RltI b2 a2 Hb2R Ha2R Hba2).
We prove the intermediate claim Hb1eq: b1 = a1.
Use symmetry.
An exact proof term for the current goal is H1eq.
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HXR2 (from left to right).
rewrite the current goal using HbEq (from left to right).
rewrite the current goal using HaEq (from left to right).
We will prove order_rel (setprod R R) (b1,b2) (a1,a2).
We will prove (setprod R R = R ∧ Rlt (b1,b2) (a1,a2)) ∨ (setprod R R = rational_numbers ∧ Rlt (b1,b2) (a1,a2)) ∨ (setprod R R = ω ∧ (b1,b2) ∈ (a1,a2)) ∨ (setprod R R = ω ∖ {0} ∧ (b1,b2) ∈ (a1,a2)) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (b1,b2) = (i,m) ∧ (a1,a2) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (b1,b2) = (c1,c2) ∧ (a1,a2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ (b1,b2) ∈ (a1,a2)).
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (b1,b2) = (c1,c2) ∧ (a1,a2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
Apply andI to the current goal.
Use reflexivity.
We use b1 to witness the existential quantifier.
We use b2 to witness the existential quantifier.
We use a1 to witness the existential quantifier.
We use a2 to witness the existential quantifier.
Apply and3I to the current goal.
Use reflexivity.
Use reflexivity.
An exact proof term for the current goal is (orIR (Rlt b1 a1) (b1 = a1 ∧ Rlt b2 a2) (andI (b1 = a1) (Rlt b2 a2) Hb1eq HbaRlt)).
An exact proof term for the current goal is (Hbap Hrel).
Assume Hba1: b1 < a1.
We prove the intermediate claim HbaRlt: Rlt b1 a1.
An exact proof term for the current goal is (RltI b1 a1 Hb1R Ha1R Hba1).
We prove the intermediate claim Hrel: order_rel X b a.
rewrite the current goal using HXR2 (from left to right).
rewrite the current goal using HbEq (from left to right).
rewrite the current goal using HaEq (from left to right).
We will prove order_rel (setprod R R) (b1,b2) (a1,a2).
We will prove (setprod R R = R ∧ Rlt (b1,b2) (a1,a2)) ∨ (setprod R R = rational_numbers ∧ Rlt (b1,b2) (a1,a2)) ∨ (setprod R R = ω ∧ (b1,b2) ∈ (a1,a2)) ∨ (setprod R R = ω ∖ {0} ∧ (b1,b2) ∈ (a1,a2)) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (b1,b2) = (i,m) ∧ (a1,a2) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (b1,b2) = (c1,c2) ∧ (a1,a2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ (b1,b2) ∈ (a1,a2)).
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (b1,b2) = (c1,c2) ∧ (a1,a2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
Apply andI to the current goal.
Use reflexivity.
We use b1 to witness the existential quantifier.
We use b2 to witness the existential quantifier.
We use a1 to witness the existential quantifier.
We use a2 to witness the existential quantifier.
Apply and3I to the current goal.
Use reflexivity.
Use reflexivity.
An exact proof term for the current goal is (orIL (Rlt b1 a1) (b1 = a1 ∧ Rlt b2 a2) HbaRlt).
An exact proof term for the current goal is (Hbap Hrel).
Assume HneqRR: ¬ (X = setprod R R).
We prove the intermediate claim HordX: ordinal X.
Apply Hso to the current goal.
Assume Hleft6.
Apply Hleft6 to the current goal.
Assume Hleft5.
Apply Hleft5 to the current goal.
Assume Hleft4.
Apply Hleft4 to the current goal.
Assume Hleft3.
Apply Hleft3 to the current goal.
Assume Hleft2.
Apply Hleft2 to the current goal.
Assume HXeq: X = R.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqR HXeq).
Assume HXeq: X = rational_numbers.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqQ HXeq).
Assume HXeq: X = ω.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqO HXeq).
Assume HXeq: X = ω ∖ {0}.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqNz HXeq).
Assume HXeq: X = setprod 2 ω.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq2 HXeq).
Assume HXeq: X = setprod R R.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqRR HXeq).
Assume Hord.
An exact proof term for the current goal is Hord.
We prove the intermediate claim HaOrd: ordinal a.
An exact proof term for the current goal is (ordinal_Hered X HordX a HaX).
We prove the intermediate claim HbOrd: ordinal b.
An exact proof term for the current goal is (ordinal_Hered X HordX b HbX).
Apply (ordinal_trichotomy_or_impred a b HaOrd HbOrd p) to the current goal.
Assume Habmem: a ∈ b.
We prove the intermediate claim Hrel: order_rel X a b.
We will prove (X = R ∧ Rlt a b) ∨ (X = rational_numbers ∧ Rlt a b) ∨ (X = ω ∧ a ∈ b) ∨ (X = ω ∖ {0} ∧ a ∈ b) ∨ (X = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (X = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ a ∈ b).
Apply orIR to the current goal.
Apply and6I to the current goal.
An exact proof term for the current goal is HordX.
An exact proof term for the current goal is HneqR.
An exact proof term for the current goal is HneqQ.
An exact proof term for the current goal is Hneq2.
An exact proof term for the current goal is HneqRR.
An exact proof term for the current goal is Habmem.
An exact proof term for the current goal is (Habp Hrel).
Assume Heq: a = b.
An exact proof term for the current goal is (Heqp Heq).
Assume Hbmem: b ∈ a.
We prove the intermediate claim Hrel: order_rel X b a.
We will prove (X = R ∧ Rlt b a) ∨ (X = rational_numbers ∧ Rlt b a) ∨ (X = ω ∧ b ∈ a) ∨ (X = ω ∖ {0} ∧ b ∈ a) ∨ (X = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ b = (i,m) ∧ a = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (X = setprod R R ∧ ∃a1 a2 b1 b2 : set, b = (a1,a2) ∧ a = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ b ∈ a).
Apply orIR to the current goal.
Apply and6I to the current goal.
An exact proof term for the current goal is HordX.
An exact proof term for the current goal is HneqR.
An exact proof term for the current goal is HneqQ.
An exact proof term for the current goal is Hneq2.
An exact proof term for the current goal is HneqRR.
An exact proof term for the current goal is Hbmem.
An exact proof term for the current goal is (Hbap Hrel).
∎