Let a and b be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

Assume Hab: a ≤ b.

Apply (RleI a b HaR HbR) to the current goal.

Assume Hlt: 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).

We prove the intermediate claim Hblta: b < a.

An exact proof term for the current goal is (RltE_lt b a Hlt).

We prove the intermediate claim Haalt: a < a.

An exact proof term for the current goal is (SNoLeLt_tra a b a HaS HbS HaS Hab Hblta).

An exact proof term for the current goal is ((SNoLt_irref a) Haalt).

∎