We will prove 0 ∈ closed_interval (minus_SNo 1) 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 Hm1le0: Rle (minus_SNo 1) 0.
An exact proof term for the current goal is (Rlt_implies_Rle (minus_SNo 1) 0 Rlt_minus1_0).
We prove the intermediate claim H0le1: Rle 0 1.
An exact proof term for the current goal is (Rlt_implies_Rle 0 1 Rlt_0_1).
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo 1) 1 0 Hm1R real_1 real_0 Hm1le0 H0le1).
∎