Let a, b and c be given.
Assume Hab: Rle a b.
Assume Hbc: Rle b c.
Apply (RleI a c (RleE_left a b Hab) (RleE_right b c Hbc)) to the current goal.
Assume Hca: Rlt c 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 HcR: c ∈ R.
An exact proof term for the current goal is (RltE_left c a Hca).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim Hncb: ¬ (Rlt c b).
An exact proof term for the current goal is (RleE_nlt b c Hbc).
Apply (SNoLt_trichotomy_or_impred c b HcS HbS False) to the current goal.
Assume Hcltb: c < b.
We will prove False.
We prove the intermediate claim Hcb: Rlt c b.
An exact proof term for the current goal is (RltI c b HcR HbR Hcltb).
An exact proof term for the current goal is (Hncb Hcb).
Assume Hceq: c = b.
We will prove False.
We prove the intermediate claim Hba: Rlt b a.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hca.
An exact proof term for the current goal is ((RleE_nlt a b Hab) Hba).
Assume Hbltc: b < c.
We will prove False.
We prove the intermediate claim HcaS: c < a.
An exact proof term for the current goal is (RltE_lt c a Hca).
We prove the intermediate claim Hbalt: b < a.
An exact proof term for the current goal is (SNoLt_tra b c a HbS HcS HaS Hbltc HcaS).
We prove the intermediate claim Hba: 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 ((RleE_nlt a b Hab) Hba).
∎