proposition: Lemma growth_rate_minus_compat: forall f g x y, D_x no_cond x y -> growth_rate (f - g)%F x y = growth_rate f x y - growth_rate g x y.
proof: Proof. intros f g x y Dxy ; unfold growth_rate, minus_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