Let x be given.

Assume Hx.

Apply nonneg_abs_SNo to the current goal.

We will prove 0 ≤ x.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Hx.

∎