proposition: Lemma derivable_pt_add : forall f1 f2 (x:C), derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 + f2) x.
proof: Proof. unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. exists (x0 + x1). apply derivable_pt_lim_add; assumption. 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