proposition: Theorem Xderive_pt_neg : forall f f' x, Xderive_pt f x f' -> Xderive_pt (fun x => Xneg (f x)) x (Xneg f').
proof: Proof. intros f f' x Hf. xtotal. intro v. apply derivable_pt_lim_eq_locally with (opp_fct (proj_fun v f)). apply locally_true_imp with (2 := derivable_imp_defined_any _ _ _ _ X Hf). intros x (w, Hw). unfold opp_fct, proj_fun. now rewrite Hw. now apply derivable_pt_lim_opp. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal