proposition: Lemma derivable_pt_lim_mirr_fwd : forall f (x l:R), derivable_pt_lim f (- x) (- l) -> derivable_pt_lim (mirr_fct f) x l.
proof: Proof. intros f x l H. change (mirr_fct f) with (comp f (opp_fct id)). replace l with ((-l) * -1) by ring. apply derivable_pt_lim_comp; [| exact H]. apply derivable_pt_lim_opp. apply derivable_pt_lim_id. Qed.
imports: Rbase Rfunctions Rlimit Rderiv