proposition: Lemma Boule_center : forall x r, Boule x r x.
proof: Proof. intros x [r rpos]; unfold Boule, Rminus; simpl; rewrite Rplus_opp_r. rewrite Rabs_pos_eq;[assumption | apply Rle_refl]. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra