proposition: Lemma derivable_pt_lim_opp : forall f (x l:R), derivable_pt_lim f x l -> derivable_pt_lim (- f) x (- l).
proof: Proof. intros f x l H. apply uniqueness_step3. unfold opp_fct, limit1_in, limit_in, dist; simpl; unfold Rdist. apply uniqueness_step2 in H. unfold limit1_in, limit_in, dist in H; simpl in H; unfold Rdist in H. intros eps Heps; specialize (H eps Heps). destruct H as [alp [Halp H]]; exists alp. split; [assumption|]. intros x0 Hx0; specialize(H x0 Hx0). rewrite <- Rabs_Ropp in H. match goal with H:Rabs(?a)<eps |- Rabs(?b)<eps => replace b with a by (field; tauto) end. assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv