proposition: Lemma derivable_pt_lim_opp : forall f x l, derivable_pt_lim f x l -> derivable_pt_lim (- f) x (- l).
proof: Proof. intros f x l H. apply uniqueness_step3. assert (H1 := uniqueness_step2 _ _ _ H). unfold opp_fct in |- * ; cut (forall h, (- f (x + h) - - f x) / h = - ((f (x + h) - f x) / h)). intro. generalize (limit_opp (fun h => (f (x + h) - f x) / h) (fun h => h <> 0) l 0 H1). unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; intros. elim (H2 eps H3); intros. exists x0. elim H4; intros. split. assumption. intros; rewrite H0; apply H6; assumption. intro; unfold Cdiv in |- *; 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