Let c and r be given.

Assume Hc: c ∈ EuclidPlane.

Assume HrR: r ∈ R.

Assume Hrpos: Rlt 0 r.

rewrite the current goal using (open_ball_EuclidPlane_metric_eq c r Hc) (from left to right).

An exact proof term for the current goal is (circular_regionI c r Hc Hrpos).

∎