Let x and y be given.

Assume HxR: x ∈ R.

Assume HyR: y ∈ R.

Assume H0lex: Rle 0 x.

We will prove Rle y (add_SNo x y).

We prove the intermediate claim HxS: SNo x.

An exact proof term for the current goal is (real_SNo x HxR).

We prove the intermediate claim HyS: SNo y.

An exact proof term for the current goal is (real_SNo y HyR).

We prove the intermediate claim Hcomm: add_SNo x y = add_SNo y x.

An exact proof term for the current goal is (add_SNo_com x y HxS HyS).

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

We prove the intermediate claim H0y: add_SNo y 0 = y.

An exact proof term for the current goal is (add_SNo_0R y HyS).

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

An exact proof term for the current goal is (Rle_add_SNo_2 y 0 x HyR real_0 HxR H0lex).

∎