proposition: Theorem Xderive_pt_mul : forall f g f' g' x, Xderive_pt f x f' -> Xderive_pt g x g' -> Xderive_pt (fun x => Xmul (f x) (g x)) x (Xadd (Xmul f' (g x)) (Xmul g' (f x))).
proof: Proof. intros f g f' g' x Hf Hg. xtotal. intro v. apply derivable_pt_lim_eq_locally with (mult_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 mult_fct, proj_fun. now rewrite Hw1, Hw2. replace r1 with (proj_fun v g r). replace r3 with (proj_fun v f r). rewrite (Rmult_comm r0). now apply derivable_pt_lim_mult. unfold proj_fun. now rewrite X0. unfold proj_fun. now rewrite X. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal