Let x be given.
Assume Hx.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using neg_abs_SNo x Hx H1 (from left to right).
We will prove abs_SNo (- x) = - x.
We prove the intermediate claim L1: 0 ≤ - x.
Apply SNoLtLe to the current goal.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is nonneg_abs_SNo (- x) L1.
Assume H1: 0 ≤ x.
Apply SNoLtLe_or (- x) 0 (SNo_minus_SNo x Hx) SNo_0 to the current goal.
Assume H2: - x < 0.
rewrite the current goal using nonneg_abs_SNo x H1 (from left to right).
rewrite the current goal using neg_abs_SNo (- x) (SNo_minus_SNo x Hx) H2 (from left to right).
We will prove - - x = x.
An exact proof term for the current goal is minus_SNo_invol x Hx.
Assume H2: 0 ≤ - x.
We prove the intermediate claim L2: x = 0.
Apply SNoLe_antisym x 0 Hx SNo_0 to the current goal.
We will prove x ≤ 0.
rewrite the current goal using minus_SNo_0 (from right to left).
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - - x ≤ - 0.
Apply minus_SNo_Le_contra 0 (- x) SNo_0 (SNo_minus_SNo x Hx) to the current goal.
We will prove 0 ≤ - x.
An exact proof term for the current goal is H2.
We will prove 0 ≤ x.
An exact proof term for the current goal is H1.
rewrite the current goal using L2 (from left to right).
Use f_equal.
An exact proof term for the current goal is minus_SNo_0.
∎