proposition: Lemma C_Rball_le : forall c r m n f, (n <= m)%nat -> C_Rball c r m f -> C_Rball c r n f.
proof: Proof. intros c r m ; induction m ; intros n f H Cmf. destruct n ; [apply Cmf | elim (Nat.nle_succ_0 _ H)]. destruct (eq_nat_dec n (S m)) as [Heq | Hneq]. subst ; assumption. apply IHm ; [| apply C_Rball_pred] ; intuition lia. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics