Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume Hypos: 0 < y.
We will prove abs_SNo (div_SNo x y) = div_SNo (abs_SNo x) y.
We prove the intermediate claim Hy0: y ≠ 0.
An exact proof term for the current goal is (SNo_pos_ne0 y HyS Hypos).
We prove the intermediate claim HdivS: SNo (div_SNo x y).
An exact proof term for the current goal is (SNo_div_SNo x y HxS HyS).
Apply (xm (0 ≤ x)) to the current goal.
Assume H0lex: 0 ≤ x.
rewrite the current goal using (nonneg_abs_SNo x H0lex) (from left to right).
We prove the intermediate claim H0lediv: 0 ≤ div_SNo x y.
Apply (SNoLt_trichotomy_or_impred (div_SNo x y) 0 HdivS SNo_0 (0 ≤ div_SNo x y)) to the current goal.
Assume Hdivlt0: div_SNo x y < 0.
We prove the intermediate claim Hxlt0': x < 0.
We prove the intermediate claim Hxlt0y: x < mul_SNo 0 y.
An exact proof term for the current goal is (div_SNo_pos_LtL' x y 0 HxS HyS SNo_0 Hypos Hdivlt0).
We will prove x < 0.
rewrite the current goal using (mul_SNo_zeroL y HyS) (from right to left) at position 1.
An exact proof term for the current goal is Hxlt0y.
We prove the intermediate claim Hxle0: x ≤ 0.
An exact proof term for the current goal is (SNoLtLe x 0 Hxlt0').
We prove the intermediate claim Heq0: x = 0.
An exact proof term for the current goal is (SNoLe_antisym x 0 HxS SNo_0 Hxle0 H0lex).
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using Heq0 (from right to left) at position 1.
An exact proof term for the current goal is Hxlt0'.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) H00) (0 ≤ div_SNo x y)).
Assume Hdiv0: div_SNo x y = 0.
rewrite the current goal using Hdiv0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0ltdiv: 0 < div_SNo x y.
An exact proof term for the current goal is (SNoLtLe 0 (div_SNo x y) H0ltdiv).
rewrite the current goal using (nonneg_abs_SNo (div_SNo x y) H0lediv) (from left to right).
Use reflexivity.
Assume Hn0lex: ¬ (0 ≤ x).
We prove the intermediate claim Hxlt0: x < 0.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (x < 0)) to the current goal.
Assume H: x < 0.
An exact proof term for the current goal is H.
Assume Hx0: x = 0.
We prove the intermediate claim H0lex: 0 ≤ x.
rewrite the current goal using Hx0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
An exact proof term for the current goal is (FalseE (Hn0lex H0lex) (x < 0)).
Assume H0ltx: 0 < x.
We prove the intermediate claim H0lex: 0 ≤ x.
An exact proof term for the current goal is (SNoLtLe 0 x H0ltx).
An exact proof term for the current goal is (FalseE (Hn0lex H0lex) (x < 0)).
rewrite the current goal using (neg_abs_SNo x HxS Hxlt0) (from left to right).
We prove the intermediate claim Hdivlt0: div_SNo x y < 0.
An exact proof term for the current goal is (div_SNo_neg_pos x y HxS HyS Hxlt0 Hypos).
rewrite the current goal using (neg_abs_SNo (div_SNo x y) HdivS Hdivlt0) (from left to right).
We prove the intermediate claim HdivNeg: div_SNo (minus_SNo x) y = minus_SNo (div_SNo x y).
Apply (mul_div_SNo_nonzero_eq (minus_SNo x) y (minus_SNo (div_SNo x y)) (SNo_minus_SNo x HxS) HyS (SNo_minus_SNo (div_SNo x y) HdivS) Hy0) to the current goal.
We prove the intermediate claim Hmul: mul_SNo y (minus_SNo (div_SNo x y)) = minus_SNo x.
rewrite the current goal using (mul_SNo_minus_distrR y (div_SNo x y) HyS HdivS) (from left to right).
rewrite the current goal using (mul_div_SNo_invR x y HxS HyS Hy0) (from left to right).
Use reflexivity.
rewrite the current goal using Hmul (from right to left) at position 1.
Use reflexivity.
rewrite the current goal using HdivNeg (from right to left) at position 1.
Use reflexivity.
∎