Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).
We prove the intermediate claim HinvR: inv_nat n ∈ R.
An exact proof term for the current goal is (inv_nat_real n HnO).
We prove the intermediate claim Hinvpos: Rlt 0 (inv_nat n).
An exact proof term for the current goal is (inv_nat_pos n HnIn).
We prove the intermediate claim Hnlt0: ¬ (Rlt (inv_nat n) 0).
An exact proof term for the current goal is (not_Rlt_sym 0 (inv_nat n) Hinvpos).
We prove the intermediate claim Hinvle1: Rle (inv_nat n) 1.
An exact proof term for the current goal is (inv_nat_Rle_1_local n HnIn).
We prove the intermediate claim Hnlt1: ¬ (Rlt 1 (inv_nat n)).
An exact proof term for the current goal is (RleE_nlt (inv_nat n) 1 Hinvle1).
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (inv_nat n) HinvR) to the current goal.
An exact proof term for the current goal is (andI (¬ (Rlt (inv_nat n) 0)) (¬ (Rlt 1 (inv_nat n))) Hnlt0 Hnlt1).
∎