Let x and y be given.

Assume Hx Hy Hxy.

Apply add_SNo_minus_Lt2b y x 0 Hy Hx SNo_0 to the current goal.

We will prove 0 + x < y.

rewrite the current goal using add_SNo_0L x Hx (from left to right).

An exact proof term for the current goal is Hxy.

∎