Let x and y be given.

Assume Hx Hy.

Let p be given.

Assume Hp1 Hp2 Hp3.

Apply SNoLt_trichotomy_or x y Hx Hy to the current goal.

Assume H.

Apply H to the current goal.

An exact proof term for the current goal is Hp1.

An exact proof term for the current goal is Hp2.

An exact proof term for the current goal is Hp3.

∎