proposition: Lemma growth_rate_inv_decomp: forall f x y, x <> y -> f x <> 0 -> f y <> 0 -> growth_rate (/ f)%F x y = - ((growth_rate f x y) * / (f x * f y)).
proof: Proof. intros ; unfold growth_rate, inv_fct ; field ; repeat split ; [| | apply Rminus_eq_contra ; symmetry ] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra