proposition: Lemma differentiable_pt_lim_opp : forall f x v l, v <> C0 -> differentiable_pt_lim f x v l -> differentiable_pt_lim (- f) x v (- l).
proof: Proof. intros f x v l v_neq H. apply uniqueness_step3. assert (H1 := uniqueness_step2 _ _ _ _ v_neq 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 u => u <> 0 /\ (exists h : R, h * u = v)) 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: Cprop_base Cnorm Ctacfield Canalysis_def