proposition: Lemma derivable_pt_mirr_prem: forall (f : R -> R) (x : R), derivable_pt (mirr_fct f) x -> derivable_pt 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_rev. repeat rewrite Ropp_involutive; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv