proposition: Lemma derivable_pt_opp : 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; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv