Let c and r be given.
Assume HcR: c ∈ R.
Assume HrR: r ∈ R.
Assume Hrgt1: Rlt 1 r.
Apply set_ext to the current goal.
Let y be given.
Assume HyB: y ∈ open_ball R R_bounded_metric c r.
We will prove y ∈ R.
An exact proof term for the current goal is (open_ballE1 R R_bounded_metric c r y HyB).
Let y be given.
Assume HyR: y ∈ R.
We will prove y ∈ open_ball R R_bounded_metric c r.
Apply (open_ballI R R_bounded_metric c r y HyR) to the current goal.
rewrite the current goal using (R_bounded_metric_apply c y HcR HyR) (from left to right).
We prove the intermediate claim Hle: Rle (R_bounded_distance c y) 1.
An exact proof term for the current goal is (R_bounded_distance_le_1 c y HcR HyR).
An exact proof term for the current goal is (Rle_Rlt_tra (R_bounded_distance c y) 1 r Hle Hrgt1).
∎