proposition: Lemma included_Rball_radiuses : forall c r r', r' <= r -> included (Rball c r') (Rball c r).
proof: Proof. intros c r r' Hr'r x x_in ; eapply Rlt_le_trans ; eassumption. Qed.
imports: Reals Rpow_facts Rfunction_def Rinterval Rextensionality Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Lra MyRIneq Rsequence_facts Rsequence_sums_facts RFsequence RFsequence_facts Rpser_def Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_sums_facts Tactics