Apply nonneg_abs_SNo to the current goal.

We will prove 0 ≤ 0.

Apply SNoLe_ref to the current goal.

∎