proposition: Theorem Xderive_pt_div : forall f g f' g' x, Xderive_pt f x f' -> Xderive_pt g x g' -> Xderive_pt (fun x => Xdiv (f x) (g x)) x (Xdiv (Xsub (Xmul f' (g x)) (Xmul g' (f x))) (Xmul (g x) (g x))).
proof: Proof. intros f g f' g' x Hf Hg. xtotal. elim Y. apply Rmult_0_l. intro v. apply derivable_pt_lim_eq_locally with (div_fct (proj_fun v f) (proj_fun v g)). generalize (derivable_imp_defined_any _ _ _ _ X0 Hf). generalize (derivable_imp_defined_ne _ _ _ _ _ X Y0 Hg). intros H2 H1. apply locally_true_imp with (2 := locally_true_and _ _ _ H1 H2). intros x ((w1, Hw1), (w2, (Hw2a, Hw2b))). unfold div_fct, proj_fun. rewrite Hw1, Hw2b. destruct (is_zero_spec w2). now elim Hw2a. apply refl_equal. replace r1 with (proj_fun v g r). replace r3 with (proj_fun v f r). fold (Rsqr (proj_fun v g r)). apply derivable_pt_lim_div. apply Hf. apply Hg. unfold proj_fun. now rewrite X. unfold proj_fun. now rewrite X0. unfold proj_fun. now rewrite X. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal