proposition: Lemma growth_rate_ext: forall f g x, f == g -> growth_rate f x == growth_rate g x.
proof: Proof. intros f g x Heq y ; unfold growth_rate ; do 2 rewrite Heq ; reflexivity. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra