Let a, b and c be given.

Assume Hab: Rle a b.

Assume Hbc: Rlt b c.

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 HcR: c ∈ R.

An exact proof term for the current goal is (RltE_right b c Hbc).

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 (Rlt a c)) to the current goal.

Assume Hablt: a < b.

We prove the intermediate claim HabRlt: Rlt a b.

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

An exact proof term for the current goal is (Rlt_tra a b c HabRlt Hbc).

Assume Habeq: a = b.

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

An exact proof term for the current goal is Hbc.

Assume Hbalt: b < a.

We prove the intermediate claim HbaRlt: Rlt b a.

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

We prove the intermediate claim Hnlt: ¬ (Rlt b a).

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

We prove the intermediate claim Hfalse: False.

An exact proof term for the current goal is (Hnlt HbaRlt).

Apply FalseE to the current goal.

An exact proof term for the current goal is Hfalse.

∎