proposition: Lemma derivable_add : forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 + f2).
proof: Proof. intros f1 f2 Hf1 Hf2 z ; apply derivable_pt_add ; intuition. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv