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