Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume Hy0: y ≠ 0.
We will prove div_SNo (minus_SNo x) y = minus_SNo (div_SNo x y).
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 (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.
∎