Let a and b be given.
Assume HaZ HbZ.
Apply iffI to the current goal.
Assume Hrel: order_rel Zplus a b.
We will prove a ∈ b.
Apply (Hrel (a ∈ b)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (a ∈ b)) to the current goal.
Assume Hleft.
Apply (Hleft (a ∈ b)) to the current goal.
Assume Hmid.
Apply (Hmid (a ∈ b)) to the current goal.
Assume Hm2.
Apply (Hm2 (a ∈ b)) to the current goal.
Assume Hm3.
Apply (Hm3 (a ∈ b)) to the current goal.
Assume Hc1.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: Zplus = R.
An exact proof term for the current goal is (andEL (Zplus = R) (Rlt a b) Hc1).
An exact proof term for the current goal is (Zplus_neq_R Heq).
Assume Hc2.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: Zplus = rational_numbers.
An exact proof term for the current goal is (andEL (Zplus = rational_numbers) (Rlt a b) Hc2).
An exact proof term for the current goal is (Zplus_neq_rational_numbers Heq).
Assume Hc3.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: Zplus = ω.
An exact proof term for the current goal is (andEL (Zplus = ω) (a ∈ b) Hc3).
An exact proof term for the current goal is (Zplus_neq_omega Heq).
Assume Hc4.
An exact proof term for the current goal is (andER (Zplus = ω ∖ {0}) (a ∈ b) Hc4).
Assume Hc5.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: Zplus = setprod 2 ω.
An exact proof term for the current goal is (andEL (Zplus = 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))) Hc5).
An exact proof term for the current goal is (Zplus_neq_setprod_2_omega Heq).
Assume Hc6.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: Zplus = setprod R R.
An exact proof term for the current goal is (andEL (Zplus = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) Hc6).
An exact proof term for the current goal is (Zplus_neq_setprod_R_R Heq).
Assume Hord: ordinal Zplus ∧ Zplus ≠ R ∧ Zplus ≠ rational_numbers ∧ Zplus ≠ setprod 2 ω ∧ Zplus ≠ setprod R R ∧ a ∈ b.
Apply Hord to the current goal.
Assume Hcore Hab2.
An exact proof term for the current goal is Hab2.
Assume Hab: a ∈ b.
We will prove order_rel Zplus a b.
We prove the intermediate claim Heq: Zplus = ω ∖ {0}.
Use reflexivity.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (mem_implies_order_rel_omega_nonzero a b Hab).
∎