proposition: Lemma derivable_pt_lim_add : forall f1 f2 x l1 l2, derivable_pt_lim f1 x l1 -> derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 + f2) x (l1 + l2).
proof: Proof. intros f1 f2 x l1 l2 H H0. apply uniqueness_step3. assert (H1 := uniqueness_step2 _ _ _ H). assert (H2 := uniqueness_step2 _ _ _ H0). unfold plus_fct in |- *. cut (forall h, (f1 (x + h) + f2 (x + h) - (f1 x + f2 x)) / h = (f1 (x + h) - f1 x) / h + (f2 (x + h) - f2 x) / h). intro H3 ; generalize (limit_plus (fun h' => (f1 (x + h') - f1 x) / h') (fun h' => (f2 (x + h') - f2 x) / h') (fun h => h <> 0) l1 l2 0 H1 H2). intros H4 eps eps_pos. elim (H4 eps eps_pos); intros x0 Hx0. exists x0. destruct Hx0 as [x0_pos Hx0']. split. assumption. intros; rewrite H3; apply Hx0'; assumption. intro; unfold Cdiv ; ring. 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