Let X, d, A, B, x and n be given.

Assume Hm: metric_on X d.

Assume HxX: x ∈ X.

Assume HB: B ∈ metric_topology X d.

Assume HxB: x ∈ B.

Assume HAcl: closed_in X (metric_topology X d) A.

Assume HAint: interior_of X (metric_topology X d) A = Empty.

Assume HnO: n ∈ ω.

We prove the intermediate claim HsuccO: ordsucc n ∈ ω.

An exact proof term for the current goal is (omega_ordsucc n HnO).

We prove the intermediate claim HaR: eps_ (ordsucc n) ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc n)) (SNo_eps_SNoS_omega (ordsucc n) HsuccO)).

We prove the intermediate claim Ha0: Rlt 0 (eps_ (ordsucc n)).

An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc n)) real_0 HaR (SNo_eps_pos (ordsucc n) HsuccO)).

An exact proof term for the current goal is (baire_step_metric_ball_bounded_closure X d A B x (eps_ (ordsucc n)) Hm HxX HB HxB HAcl HAint HaR Ha0).

∎