proposition: Lemma growth_rate_mult_real_fct_compat: forall f (l:R) x y, D_x no_cond x y -> growth_rate (mult_real_fct l f)%F x y = l * growth_rate f x y.
proof: Proof. intros f l x y Dxy ; unfold growth_rate, mult_real_fct ; field ; apply Rminus_eq_contra ; symmetry ; apply Dxy. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra