Let x be given.

Assume Hx1 Hx2.

Apply not_nonneg_abs_SNo to the current goal.

Assume H1: 0 ≤ x.

We will prove False.

Apply SNoLt_irref x to the current goal.

We will prove x < x.

An exact proof term for the current goal is SNoLtLe_tra x 0 x Hx1 SNo_0 Hx1 Hx2 H1.

∎