Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Hy.
We prove the intermediate claim Lmw: SNo (- w).
An exact proof term for the current goal is SNo_minus_SNo w Hw.
rewrite the current goal using SNo_foil x (- y) z (- w) Hx Lmy Hz Lmw (from left to right).
We will prove x * z + x * (- w) + (- y) * z + (- y) * (- w) = x * z + - x * w + - y * z + y * w.
rewrite the current goal using mul_SNo_minus_minus y w Hy Hw (from left to right).
rewrite the current goal using mul_SNo_minus_distrL y z Hy Hz (from left to right).
rewrite the current goal using mul_SNo_minus_distrR x w Hx Hw (from left to right).
Use reflexivity.
∎