Let x, r and y be given.
Assume HxR: x ∈ R.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hrlt1: Rlt r 1.
Assume HyB: y ∈ open_ball R R_bounded_metric x r.
We prove the intermediate claim Hpair: y ∈ R ∧ Rlt (R_bounded_distance x y) r.
An exact proof term for the current goal is (iffEL (y ∈ open_ball R R_bounded_metric x r) (y ∈ R ∧ Rlt (R_bounded_distance x y) r) (open_ball_R_bounded_metric_abs_early x r y HxR HrR Hrpos Hrlt1) HyB).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (andEL (y ∈ R) (Rlt (R_bounded_distance x y) r) Hpair).
We prove the intermediate claim Hbdlt: Rlt (R_bounded_distance x y) r.
An exact proof term for the current goal is (andER (y ∈ R) (Rlt (R_bounded_distance x y) r) Hpair).
An exact proof term for the current goal is (R_bounded_distance_lt_lt1_imp_abs_lt x y r HxR HyR HrR Hrlt1 Hbdlt).
∎