proposition: Lemma growth_rate_ext_strong: forall (D : R -> Prop) f g x, D x -> (forall x, D x -> f x = g x) -> forall y, D y -> growth_rate f x y = growth_rate g x y.
proof: Proof. intros D f g x Dx Heq y y_in ; unfold growth_rate ; do 2 (rewrite Heq ; [| assumption]) ; reflexivity. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra