proposition: Lemma derive_pt_inv : forall (f:R -> R) (x:R) (pr:derivable_pt f x) (na:f x <> 0), derive_pt (/ f) x (derivable_pt_inv f x na pr) = - derive_pt f x pr / Rsqr (f x).
proof: Proof. intros; replace (derive_pt (/ f) x (derivable_pt_inv f x na pr)) with (derive_pt (fct_cte 1 / f) x (derivable_pt_div (fct_cte 1) f x (derivable_pt_const 1 x) pr na)). - rewrite derive_pt_div; rewrite derive_pt_const; unfold fct_cte; rewrite Rmult_0_l; rewrite Rmult_1_r; unfold Rminus; rewrite Rplus_0_l; reflexivity. - apply pr_nu_var2. intro; unfold div_fct, fct_cte, inv_fct. unfold Rdiv; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia