Let a and b be given.

Assume Hab: Rle a b.

Assume Hba: Rle b a.

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 Hnltab: ¬ (Rlt a b).

An exact proof term for the current goal is (RleE_nlt b a Hba).

We prove the intermediate claim Hnltba: ¬ (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 (a = b)) to the current goal.

Assume Hablt: a < b.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hnltab (RltI a b HaR HbR Hablt)).

Assume HabEq: a = b.

An exact proof term for the current goal is HabEq.

Assume Hbalt: b < a.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hnltba (RltI b a HbR HaR Hbalt)).

∎