Let x be given.

Assume Hx Hx1.

rewrite the current goal using add_SNo_1_1_2 (from right to left).

We will prove x + 1 < (1 + 1) * x.

rewrite the current goal using mul_SNo_distrR 1 1 x SNo_1 SNo_1 Hx (from left to right).

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

We will prove x + 1 < x + x.

Apply add_SNo_Lt2 x 1 x Hx SNo_1 Hx to the current goal.

We will prove 1 < x.

An exact proof term for the current goal is Hx1.

∎