Let x be given.
Assume HxR.
Set a0 to be the term add_SNo x (minus_SNo 1).
Set b0 to be the term add_SNo x 1.
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR (minus_SNo 1) Hm1R).
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
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 Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is (real_SNo 1 real_1).
We prove the intermediate claim Ha0ltx: a0 < x.
We prove the intermediate claim Hlt: a0 < add_SNo x 0.
An exact proof term for the current goal is (add_SNo_Lt2 x (minus_SNo 1) 0 HxS Hm1S SNo_0 minus_1_lt_0).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 2.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hxltb0: x < b0.
We prove the intermediate claim Hlt: add_SNo x 0 < b0.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS SNo_0 H1S SNoLt_0_1).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Ha0x: Rlt a0 x.
An exact proof term for the current goal is (RltI a0 x Ha0R HxR Ha0ltx).
We prove the intermediate claim Hxb0: Rlt x b0.
An exact proof term for the current goal is (RltI x b0 HxR Hb0R Hxltb0).
We prove the intermediate claim Hconj: Rlt a0 x ∧ Rlt x b0.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0x.
An exact proof term for the current goal is Hxb0.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a0 x0 ∧ Rlt x0 b0) x HxR Hconj).
∎