proposition: Lemma derivable_inv : forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f).
proof: Proof. intros f H X. unfold derivable; intro x. apply derivable_pt_inv. - apply (H x). - apply (X x). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia