Let x, y and z be given.
Assume Hx Hy Hz.
We prove the intermediate claim Lxdy: SNo (x :/: y).
An exact proof term for the current goal is SNo_div_SNo x y Hx Hy.
We prove the intermediate claim Lxdydz: SNo ((x :/: y) :/: z).
An exact proof term for the current goal is SNo_div_SNo (x :/: y) z Lxdy Hz.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lyz: SNo (y * z).
An exact proof term for the current goal is SNo_mul_SNo y z Hy Hz.
We prove the intermediate claim Lxdyz: SNo (x :/: (y * z)).
An exact proof term for the current goal is SNo_div_SNo x (y * z) Hx Lyz.
Apply xm (y = 0) to the current goal.
Assume Hy0: y = 0.
rewrite the current goal using Hy0 (from left to right).
We will prove (x :/: 0) :/: z = x :/: (0 * z).
rewrite the current goal using mul_SNo_zeroL z Hz (from left to right).
rewrite the current goal using div_SNo_0_denum x Hx (from left to right).
We will prove 0 :/: z = 0.
An exact proof term for the current goal is div_SNo_0_num z Hz.
Assume Hy0: y ≠ 0.
Apply xm (z = 0) to the current goal.
Assume Hz0: z = 0.
rewrite the current goal using Hz0 (from left to right).
We will prove (x :/: y) :/: 0 = x :/: (y * 0).
rewrite the current goal using mul_SNo_zeroR y Hy (from left to right).
We will prove (x :/: y) :/: 0 = x :/: 0.
rewrite the current goal using div_SNo_0_denum x Hx (from left to right).
An exact proof term for the current goal is div_SNo_0_denum (x :/: y) Lxdy.
Assume Hz0: z ≠ 0.
We prove the intermediate claim Lyz0: y * z ≠ 0.
Assume H1: y * z = 0.
Apply Hz0 to the current goal.
We will prove z = 0.
Apply mul_SNo_nonzero_cancel y z 0 Hy Hy0 Hz SNo_0 to the current goal.
We will prove y * z = y * 0.
rewrite the current goal using mul_SNo_zeroR y Hy (from left to right).
An exact proof term for the current goal is H1.
Apply mul_SNo_nonzero_cancel z ((x :/: y) :/: z) (x :/: (y * z)) Hz Hz0 Lxdydz Lxdyz to the current goal.
rewrite the current goal using mul_div_SNo_invR (x :/: y) z Lxdy Hz Hz0 (from left to right).
We will prove x :/: y = z * (x :/: (y * z)).
Apply mul_SNo_nonzero_cancel y (x :/: y) (z * (x :/: (y * z))) Hy Hy0 Lxdy (SNo_mul_SNo z (x :/: (y * z)) Hz Lxdyz) to the current goal.
rewrite the current goal using mul_div_SNo_invR x y Hx Hy Hy0 (from left to right).
We will prove x = y * z * (x :/: (y * z)).
rewrite the current goal using mul_SNo_assoc y z (x :/: (y * z)) Hy Hz Lxdyz (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_div_SNo_invR x (y * z) Hx Lyz Lyz0.
∎