Let a and b be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

Assume Hnltab: ¬ (Rlt a b).

Assume Hnltba: ¬ (Rlt b a).

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).

Apply (SNoLt_trichotomy_or_impred a b HaS HbS (a = b)) to the current goal.

Assume Hab: a < b.

We prove the intermediate claim Hr: Rlt a b.

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

An exact proof term for the current goal is (FalseE (Hnltab Hr) (a = b)).

Assume Heq: a = b.

An exact proof term for the current goal is Heq.

Assume Hba: b < a.

We prove the intermediate claim Hr: Rlt b a.

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

An exact proof term for the current goal is (FalseE (Hnltba Hr) (a = b)).

∎