Let x, y and z be given.

Assume Hx Hy Hz.

rewrite the current goal using add_SNo_com x y Hx Hy (from left to right).

rewrite the current goal using add_SNo_com x z Hx Hz (from left to right).

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

∎