Let x, y and z be given.

Assume Hx Hy Hz.

Apply SNo_add_SNo_3 to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is Hy.

Apply SNo_minus_SNo to the current goal.

An exact proof term for the current goal is Hz.

∎