Let s be given.
Assume HsI: s ∈ open_interval (minus_SNo 1) 1.
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim HmsR: minus_SNo s ∈ R.
An exact proof term for the current goal is (real_minus_SNo s HsR).
We prove the intermediate claim Hbds: Rlt (minus_SNo 1) s ∧ Rlt s 1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim Hm1lts: Rlt (minus_SNo 1) s.
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hslt1: Rlt s 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) s) (Rlt s 1) Hbds).
We prove the intermediate claim Hmslt1: Rlt (minus_SNo s) 1.
We prove the intermediate claim Hmslt1S: minus_SNo s < 1.
We prove the intermediate claim Hmslt1S': minus_SNo s < minus_SNo (minus_SNo 1).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo 1) s (SNo_minus_SNo 1 SNo_1) (real_SNo s HsR) (RltE_lt (minus_SNo 1) s Hm1lts)).
rewrite the current goal using (minus_SNo_invol 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is Hmslt1S'.
An exact proof term for the current goal is (RltI (minus_SNo s) 1 HmsR real_1 Hmslt1S).
We prove the intermediate claim Hm1ltms: Rlt (minus_SNo 1) (minus_SNo s).
We prove the intermediate claim Hm1ltmsS: minus_SNo 1 < minus_SNo s.
An exact proof term for the current goal is (minus_SNo_Lt_contra s 1 (real_SNo s HsR) SNo_1 (RltE_lt s 1 Hslt1)).
An exact proof term for the current goal is (RltI (minus_SNo 1) (minus_SNo s) (real_minus_SNo 1 real_1) HmsR Hm1ltmsS).
We prove the intermediate claim HIdef: open_interval (minus_SNo 1) 1 = {x0 ∈ R|Rlt (minus_SNo 1) x0 ∧ Rlt x0 1}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
Apply (SepI R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) (minus_SNo s) HmsR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hm1ltms.
An exact proof term for the current goal is Hmslt1.
∎