Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
Use transitivity with (x + y) * z + (x + y) * w, (x * z + y * z) + (x + y) * w, and (x * z + y * z) + (x * w + y * w).
An exact proof term for the current goal is mul_SNo_distrL (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw.
Use f_equal.
An exact proof term for the current goal is mul_SNo_distrR x y z Hx Hy Hz.
Use f_equal.
An exact proof term for the current goal is mul_SNo_distrR x y w Hx Hy Hw.
We will prove (x * z + y * z) + (x * w + y * w) = x * z + (x * w + (y * z + y * w)).
rewrite the current goal using add_SNo_com_4_inner_mid (x * z) (y * z) (x * w) (y * w) (SNo_mul_SNo x z Hx Hz) (SNo_mul_SNo y z Hy Hz) (SNo_mul_SNo x w Hx Hw) (SNo_mul_SNo y w Hy Hw) (from left to right).
We will prove (x * z + x * w) + (y * z + y * w) = x * z + (x * w + (y * z + y * w)).
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc (x * z) (x * w) (y * z + y * w) (SNo_mul_SNo x z Hx Hz) (SNo_mul_SNo x w Hx Hw) (SNo_add_SNo (y * z) (y * w) (SNo_mul_SNo y z Hy Hz) (SNo_mul_SNo y w Hy Hw)).
∎