proposition: Lemma derivable_pt_mirr: forall (f : R -> R) (x : R), derivable_pt f (-x) -> derivable_pt (mirr_fct f) x.
proof: Proof. intros f x H. unfold derivable_pt in H. destruct H as [l H]; exists (-l). apply derivable_pt_lim_mirr_fwd. rewrite Ropp_involutive; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv