Let x, r and y be given.
Assume Hx: x ∈ R.
Assume Hr: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hrlt1: Rlt r 1.
Apply iffI to the current goal.
Assume HyB: y ∈ open_ball R R_bounded_metric x r.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (open_ballE1 R R_bounded_metric x r y HyB).
We prove the intermediate claim Hlt: Rlt (apply_fun R_bounded_metric (x,y)) r.
An exact proof term for the current goal is (open_ballE2 R R_bounded_metric x r y HyB).
Apply andI to the current goal.
An exact proof term for the current goal is HyR.
We will prove Rlt (R_bounded_distance x y) r.
rewrite the current goal using (R_bounded_metric_apply x y Hx HyR) (from right to left).
An exact proof term for the current goal is Hlt.
Assume Hpair: y ∈ R ∧ Rlt (R_bounded_distance x y) r.
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 Hlt: 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).
Apply (open_ballI R R_bounded_metric x r y HyR) to the current goal.
rewrite the current goal using (R_bounded_metric_apply x y Hx HyR) (from left to right).
An exact proof term for the current goal is Hlt.
∎