proposition: Lemma derivable_pt_inv : forall (f:R -> R) (x:R), f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x.
proof: Proof. intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). - intro X0; apply X0. apply derivable_pt_div. + apply derivable_pt_const. + assumption. + assumption. - unfold div_fct, inv_fct, fct_cte; intros (x0,p); unfold derivable_pt; exists x0; unfold derivable_pt_abs; unfold derivable_pt_lim; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; intros; elim (p eps H0); intros; exists x1; intros; unfold Rdiv in H1; unfold Rdiv; rewrite <- (Rmult_1_l (/ f x)); rewrite <- (Rmult_1_l (/ f (x + h))). apply H1; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia