proposition: Lemma derive_pt_mirr_rev : forall f (x:R) (pr1:derivable_pt (mirr_fct f) x), derive_pt (mirr_fct f) x pr1 = - derive_pt f (-x) (derivable_pt_mirr_prem f x pr1).
proof: Proof. intros. apply derive_pt_eq_0. apply derivable_pt_lim_mirr_fwd. rewrite Ropp_involutive. apply (derive_pt_eq_1 _ _ _ (derivable_pt_mirr_prem f x pr1)). reflexivity. Qed.
imports: Rbase Rfunctions Rlimit Rderiv