Let t be given.
Assume HtR: t ∈ R.
Assume H1let: Rle 1 t.
Assume H0ltt: Rlt 0 t.
We will prove recip_SNo_pos t ∈ unit_interval.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim H0lttS: 0 < t.
An exact proof term for the current goal is (RltE_lt 0 t H0ltt).
We prove the intermediate claim H1letS: 1 ≤ t.
An exact proof term for the current goal is (SNoLe_of_Rle 1 t H1let).
We prove the intermediate claim HinvR: recip_SNo_pos t ∈ R.
An exact proof term for the current goal is (real_recip_SNo_pos t HtR H0lttS).
We prove the intermediate claim HinvS: SNo (recip_SNo_pos t).
An exact proof term for the current goal is (real_SNo (recip_SNo_pos t) HinvR).
We prove the intermediate claim HinvposS: 0 < recip_SNo_pos t.
An exact proof term for the current goal is (recip_SNo_pos_is_pos t HtS H0lttS).
We prove the intermediate claim Hnltinv0: ¬ (Rlt (recip_SNo_pos t) 0).
An exact proof term for the current goal is (not_Rlt_sym 0 (recip_SNo_pos t) (RltI 0 (recip_SNo_pos t) real_0 HinvR HinvposS)).
We prove the intermediate claim Hinvle1S: recip_SNo_pos t ≤ 1.
An exact proof term for the current goal is (recip_SNo_pos_le1_of_ge1 t HtS H0lttS H1letS).
We prove the intermediate claim Hinvle1: Rle (recip_SNo_pos t) 1.
An exact proof term for the current goal is (Rle_of_SNoLe (recip_SNo_pos t) 1 HinvR real_1 Hinvle1S).
We prove the intermediate claim Hnlt1inv: ¬ (Rlt 1 (recip_SNo_pos t)).
An exact proof term for the current goal is (RleE_nlt (recip_SNo_pos t) 1 Hinvle1).
An exact proof term for the current goal is (SepI R (λu : set ⇒ ¬ (Rlt u 0) ∧ ¬ (Rlt 1 u)) (recip_SNo_pos t) HinvR (andI (¬ (Rlt (recip_SNo_pos t) 0)) (¬ (Rlt 1 (recip_SNo_pos t))) Hnltinv0 Hnlt1inv)).
∎