Let x, y and z be given.
Assume HxR: x ∈ R.
Assume HyR: y ∈ R.
Assume HzR: z ∈ R.
Assume Hyz: Rle y z.
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 HxyR: add_SNo x y ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR y HyR).
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).
Apply (RleI (add_SNo x y) (add_SNo x z) HxyR HxzR) to the current goal.
Assume Hlt: Rlt (add_SNo x z) (add_SNo x y).
We prove the intermediate claim HltS: add_SNo x z < add_SNo x y.
An exact proof term for the current goal is (RltE_lt (add_SNo x z) (add_SNo x y) Hlt).
We prove the intermediate claim Hzly: z < y.
An exact proof term for the current goal is (add_SNo_Lt2_cancel x z y HxS HzS HyS HltS).
We prove the intermediate claim Hzy: Rlt z y.
An exact proof term for the current goal is (RltI z y HzR HyR Hzly).
An exact proof term for the current goal is ((RleE_nlt y z Hyz) Hzy).
∎