Let a and b be given.
Assume Hab.
We will prove order_rel (ω ∖ {0}) a b.
We will prove (ω ∖ {0} = R ∧ Rlt a b) ∨ (ω ∖ {0} = rational_numbers ∧ Rlt a b) ∨ (ω ∖ {0} = ω ∧ a ∈ b) ∨ (ω ∖ {0} = ω ∖ {0} ∧ a ∈ b) ∨ (ω ∖ {0} = 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))) ∨ (ω ∖ {0} = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal (ω ∖ {0}) ∧ (ω ∖ {0}) ≠ R ∧ (ω ∖ {0}) ≠ rational_numbers ∧ (ω ∖ {0}) ≠ setprod 2 ω ∧ (ω ∖ {0}) ≠ setprod R R ∧ a ∈ b).
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove ω ∖ {0} = ω ∖ {0} ∧ a ∈ b.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hab.
∎