proposition: Lemma growth_rate_mult_decomp: forall f g x y, x <> y -> growth_rate (f * g)%F x y = (growth_rate f x y) * g x + f y * growth_rate g x y.
proof: Proof. intros f g x y Hneq ; unfold growth_rate, mult_fct ; field ; apply Rminus_eq_contra ; symmetry ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra