Let a and b be given.
Assume Hab: Rle a b.
Assume Hneq: ¬ (a = b).
We will prove Rlt a b.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RleE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RleE_right a b Hab).
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).
We prove the intermediate claim Hnlt: ¬ (Rlt b a).
An exact proof term for the current goal is (RleE_nlt a b Hab).
Apply (SNoLt_trichotomy_or_impred a b HaS HbS (Rlt a b)) to the current goal.
Assume Hablt: a < b.
We will prove a ∈ R ∧ b ∈ R ∧ a < b.
Apply and3I to the current goal.
An exact proof term for the current goal is HaR.
An exact proof term for the current goal is HbR.
An exact proof term for the current goal is Hablt.
Assume Habeq: a = b.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Habeq).
Assume Hblt: b < a.
We prove the intermediate claim Hba: Rlt b a.
We will prove b ∈ R ∧ a ∈ R ∧ b < a.
Apply and3I to the current goal.
An exact proof term for the current goal is HbR.
An exact proof term for the current goal is HaR.
An exact proof term for the current goal is Hblt.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt Hba).
∎