Let x, y and z be given.

Assume Hx Hy Hz.

Use transitivity with and - x + - (y + z).

An exact proof term for the current goal is minus_add_SNo_distr x (y + z) Hx (SNo_add_SNo y z Hy Hz).

Use f_equal.

We will prove - (y + z) = - y + - z.

An exact proof term for the current goal is minus_add_SNo_distr y z Hy Hz.

∎