We prove the intermediate claim L1: ∀x y z, SNo x → SNo y → SNo z → (x + y) + z = x + (y + z).

Let x, y and z be given.

Assume Hx Hy Hz.

Use symmetry.

An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.

An exact proof term for the current goal is CD_add_mul_distrR {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo SNo_minus_SNo (λx H ⇒ H) SNo_add_SNo SNo_mul_SNo minus_add_SNo_distr L1 add_SNo_com mul_SNo_distrL mul_SNo_distrR.

∎