Let x, y and z be given.
Assume HxR: x ∈ R.
Assume HyR: y ∈ R.
Assume HzR: z ∈ R.
Assume Hxy: Rle 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 HzS: SNo z.
An exact proof term for the current goal is (real_SNo z HzR).
We prove the intermediate claim HxzR: add_SNo x z ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR z HzR).
We prove the intermediate claim HyzR: add_SNo y z ∈ R.
An exact proof term for the current goal is (real_add_SNo y HyR z HzR).
We prove the intermediate claim Hcomm_xz: add_SNo x z = add_SNo z x.
An exact proof term for the current goal is (add_SNo_com x z HxS HzS).
We prove the intermediate claim Hcomm_yz: add_SNo y z = add_SNo z y.
An exact proof term for the current goal is (add_SNo_com y z HyS HzS).
rewrite the current goal using Hcomm_xz (from left to right).
rewrite the current goal using Hcomm_yz (from left to right).
An exact proof term for the current goal is (Rle_add_SNo_2 z x y HzR HxR HyR Hxy).
∎