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