proposition: Lemma derivable_pt_lim_mirr_rev : forall f (x l:R), derivable_pt_lim (mirr_fct 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 => (mirr_fct f (- x))). - intros; unfold mirr_fct; rewrite Ropp_involutive; reflexivity. - apply derivable_pt_lim_mirr_fwd; exact H. Qed.
imports: Rbase Rfunctions Rlimit Rderiv