Let a and b be given.

Assume Hab: Rle a b.

We will prove 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 (a ≤ b)) to the current goal.

Assume Hablt: a < b.

An exact proof term for the current goal is (SNoLtLe a b Hablt).

Assume Habeq: a = b.

rewrite the current goal using Habeq (from left to right).

An exact proof term for the current goal is (SNoLe_ref b).

Assume Hbalt: b < a.

We prove the intermediate claim HbaltR: Rlt b a.

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

An exact proof term for the current goal is (FalseE (Hnlt HbaltR) (a ≤ b)).

∎