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 HsS: SNo s.
An exact proof term for the current goal is (real_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 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 Hslt1S: s < 1.
An exact proof term for the current goal is (RltE_lt s 1 Hslt1).
Apply (xm (0 ≤ s)) to the current goal.
Assume H0les: 0 ≤ s.
rewrite the current goal using (nonneg_abs_SNo s H0les) (from left to right).
An exact proof term for the current goal is Hslt1S.
Assume Hn0les: ¬ (0 ≤ s).
We prove the intermediate claim Hslt0: s < 0.
Apply (SNoLt_trichotomy_or_impred s 0 HsS SNo_0 (s < 0)) to the current goal.
Assume H: s < 0.
An exact proof term for the current goal is H.
Assume Hs0: s = 0.
We prove the intermediate claim H0les: 0 ≤ s.
rewrite the current goal using Hs0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
An exact proof term for the current goal is (FalseE (Hn0les H0les) (s < 0)).
Assume H0lts: 0 < s.
We prove the intermediate claim H0les: 0 ≤ s.
An exact proof term for the current goal is (SNoLtLe 0 s H0lts).
An exact proof term for the current goal is (FalseE (Hn0les H0les) (s < 0)).
rewrite the current goal using (not_nonneg_abs_SNo s Hn0les) (from left to right).
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 Hm1ltsS: minus_SNo 1 < s.
An exact proof term for the current goal is (RltE_lt (minus_SNo 1) s Hm1lts).
We prove the intermediate claim HmsLt1': 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) HsS Hm1ltsS).
We prove the intermediate claim HmsLt1: minus_SNo s < 1.
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 HmsLt1'.
An exact proof term for the current goal is HmsLt1.
∎