proposition: Lemma growth_rate_Cre : forall (f : C -> C) lb ub f', (lb <> ub)%R -> Rabs (Ranalysis_def.growth_rate (fun z => Cre (f z)) lb ub - Cre f')%R <= Cnorm (growth_rate f lb ub - f')%C.
proof: Proof. intros f lb ub f' ublb_neq ; unfold Ranalysis_def.growth_rate ; rewrite Cre_minus_compat, <- Cre_div_compat, Cre_minus_compat. + etransitivity. - eapply Cre_le_Cnorm. - rewrite <- IRC_minus_compat ; reflexivity. + apply Rminus_eq_contra ; symmetry ; assumption. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv