Let x and y be given.

Assume Hx Hy.

Apply SNoLt_trichotomy_or x y Hx Hy to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1: x < y.

Apply orIL to the current goal.

An exact proof term for the current goal is H1.

Assume H1: x = y.

Apply orIR to the current goal.

We will prove y ≤ x.

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

We will prove y ≤ y.

Apply SNoLe_ref to the current goal.

Assume H1: y < x.

Apply orIR to the current goal.

We will prove y ≤ x.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is H1.

∎