Let a, b and c be given.

Assume Hab: Rlt a b.

Assume Hbc: Rle b c.

We prove the intermediate claim HaR: a ∈ R.

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

We prove the intermediate claim HbR: b ∈ R.

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

We prove the intermediate claim HcR: c ∈ R.

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

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 HcS: SNo c.

An exact proof term for the current goal is (real_SNo c HcR).

Apply (SNoLt_trichotomy_or_impred b c HbS HcS (Rlt a c)) to the current goal.

Assume Hbltc: b < c.

We prove the intermediate claim HbcRlt: Rlt b c.

An exact proof term for the current goal is (RltI b c HbR HcR Hbltc).

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

Assume Hbeq: b = c.

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

An exact proof term for the current goal is Hab.

Assume Hcltb: c < b.

We prove the intermediate claim HcbRlt: Rlt c b.

An exact proof term for the current goal is (RltI c b HcR HbR Hcltb).

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

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

An exact proof term for the current goal is (FalseE (Hnlt HcbRlt) (Rlt a c)).

∎