proposition: Lemma Rball_ext_eq: forall c1 c2 r1 r2, r1 > 0 -> (forall x, Rball c1 r1 x <-> Rball c2 r2 x) -> c1 = c2 /\ r1 = r2.
proof: Proof. intros c1 c2 r1 r2 r1_pos Hext. assert (Hord: c1 - r1 < c1 + r1) by lra. assert (Heq: c1 - r1 = c2 - r2 /\ c1 + r1 = c2 + r2). apply open_interval_ext_eq. assumption. intro x ; split ; intro H ; eapply included_Rball_open_interval, Hext, included_open_interval_Rball2 ; assumption. split. replace c1 with ((c1 - r1 + (c1 + r1)) / 2) by field ; replace c2 with ((c2 - r2 + (c2 + r2)) / 2) by field ; destruct Heq as [H1 H2] ; rewrite H1, H2 ; field. replace r1 with ((c1 + r1 - (c1 - r1)) / 2) by field ; replace r2 with ((c2 + r2 - (c2 - r2)) / 2) by field ; destruct Heq as [H1 H2] ; rewrite H1, H2 ; field. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics