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