Let x and y be given.
Assume HxR: x ∈ R.
Assume HyR: y ∈ R.
Assume Hy0: y ≠ 0.
We will prove div_SNo x (minus_SNo y) = minus_SNo (div_SNo x y).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
Set z to be the term div_SNo x y.
We prove the intermediate claim HzR: z ∈ R.
An exact proof term for the current goal is (real_div_SNo x HxR y HyR).
We prove the intermediate claim HzS: SNo z.
An exact proof term for the current goal is (real_SNo z HzR).
We prove the intermediate claim HmyS: SNo (minus_SNo y).
An exact proof term for the current goal is (SNo_minus_SNo y HyS).
We prove the intermediate claim HmzS: SNo (minus_SNo z).
An exact proof term for the current goal is (SNo_minus_SNo z HzS).
We prove the intermediate claim Hmy0: (minus_SNo y) ≠ 0.
Assume Hmy0eq: minus_SNo y = 0.
We prove the intermediate claim Hy0eq: y = 0.
rewrite the current goal using (minus_SNo_minus_SNo_R y HyR) (from right to left).
rewrite the current goal using Hmy0eq (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hy0 Hy0eq).
We prove the intermediate claim HyzR: mul_SNo y z ∈ R.
An exact proof term for the current goal is (real_mul_SNo y HyR z HzR).
We prove the intermediate claim Hminus_mul: mul_SNo (minus_SNo y) (minus_SNo z) = mul_SNo y z.
rewrite the current goal using (mul_SNo_minus_distrL y (minus_SNo z) HyS HmzS) (from left to right).
rewrite the current goal using (mul_SNo_minus_distrR y z HyS HzS) (from left to right).
rewrite the current goal using (minus_SNo_minus_SNo_R (mul_SNo y z) HyzR) (from left to right).
Use reflexivity.
We prove the intermediate claim Hmul0: mul_SNo y z = x.
An exact proof term for the current goal is (mul_div_SNo_invR x y HxS HyS Hy0).
We prove the intermediate claim Hmul: x = mul_SNo (minus_SNo y) (minus_SNo z).
rewrite the current goal using Hminus_mul (from left to right) at position 1.
rewrite the current goal using Hmul0 (from left to right) at position 1.
Use reflexivity.
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq x (minus_SNo y) (minus_SNo z) HxS HmyS HmzS Hmy0 Hmul).
∎