Let x and y be given.

Assume HxS: SNo x.

Assume HyS: SNo y.

Assume H0ley: 0 ≤ y.

We prove the intermediate claim H0S: SNo 0.

An exact proof term for the current goal is SNo_0.

We prove the intermediate claim Hle: add_SNo x 0 ≤ add_SNo x y.

An exact proof term for the current goal is (add_SNo_Le2 x 0 y HxS H0S HyS H0ley).

We prove the intermediate claim Hx0: add_SNo x 0 = x.

An exact proof term for the current goal is (add_SNo_0R x HxS).

We will prove x ≤ add_SNo x y.

rewrite the current goal using Hx0 (from right to left) at position 1.

An exact proof term for the current goal is Hle.

∎