We will prove closed_in (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) ((closed_interval one_third 1) ∩ (closed_interval (minus_SNo 1) 1)).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Hm1real: (minus_SNo 1) ∈ real.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1R: (minus_SNo 1) ∈ R.
rewrite the current goal using HdefR (from left to right) at position 1.
An exact proof term for the current goal is Hm1real.
We prove the intermediate claim H1R: 1 ∈ R.
rewrite the current goal using HdefR (from left to right) at position 1.
An exact proof term for the current goal is real_1.
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
An exact proof term for the current goal is (closed_interval_closed_in_closed_interval_topology (minus_SNo 1) 1 one_third 1 Hm1R H1R H13R H1R).
∎