proposition: Lemma derivable_pt_lim_opp_rev : 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 derivable_pt_lim_ext with (f := fun x => - - (f x)). - intros; rewrite Ropp_involutive; reflexivity. - apply derivable_pt_lim_opp_fwd; exact H. Qed.
imports: Rbase Rfunctions Rlimit Rderiv