proposition: Theorem Xderive_pt_sub : forall f g f' g' x, Xderive_pt f x f' -> Xderive_pt g x g' -> Xderive_pt (fun x => Xsub (f x) (g x)) x (Xsub f' g').
proof: Proof. intros f g f' g' x Hf Hg. xtotal. intro v. apply derivable_pt_lim_eq_locally with (minus_fct (proj_fun v f) (proj_fun v g)). apply locally_true_imp with (2 := derivable_imp_defined_any_2 _ _ _ _ _ _ _ X0 X Hf Hg). intros x ((w1, Hw1), (w2, Hw2)). unfold minus_fct, proj_fun. now rewrite Hw1, Hw2. now apply derivable_pt_lim_minus. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal