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