proposition: Lemma Dmult : forall (D:C -> Prop) (df dg f g:C -> C) (z:C), D_in f df D z -> D_in g dg D z -> D_in (fun z:C => f z * g z) (fun z:C => df z * g z + f z * dg z) D z.
proof: Proof. intros; unfold D_in in |- *; generalize H H0; intros; unfold D_in in H, H0; generalize (cont_deriv f df D z H1); unfold continue_in in |- *; intro; generalize (limit_mul (fun x:C => (g x - g z) * / (x - z)) ( fun z:C => f z) (D_x D z) (dg z) (f z) z H0 H3); intro; cut (limit1_in (fun x:C => g z) (D_x D z) (g z) z). intro; generalize (limit_mul (fun x:C => (f x - f z) * / (x - z)) ( fun _:C => g z) (D_x D z) (df z) (g z) z H H5); clear H H0 H1 H2 H3 H5; intro; generalize (limit_plus (fun x:C => (f x - f z) * / (x - z) * g z) (fun x:C => (g x - g z) * / (x - z) * f x) ( D_x D z) (df z * g z) (dg z * f z) z H H4); clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H; simpl in H; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; split with x; split; auto; intros; generalize (H1 x0 H2); clear H1; intro; rewrite (Cmult_comm (f x0 - f z) (/ (x0 - z))) in H1; rewrite (Cmult_comm (g x0 - g z) (/ (x0 - z))) in H1; rewrite (Cmult_assoc (/ (x0 - z)) (f x0 - f z) (g z)) in H1; rewrite (Cmult_assoc (/ (x0 - z)) (g x0 - g z) (f x0)) in H1. rewrite <- (Cmult_add_distr_l (/ (x0 - z)) ((f x0 - f z) * g z) ((g x0 - g z) * f x0)) in H1; rewrite (Cmult_comm (/ (x0 - z)) ((f x0 - f z) * g z + (g x0 - g z) * f x0)) in H1; rewrite (Cmult_comm (dg z) (f z)) in H1; cut ((f x0 - f z) * g z + (g x0 - g z) * f x0 = f x0 * g x0 - f z * g z). intro; rewrite H3 in H1; assumption. ring. unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; split with eps; split; auto; intros; elim (C_dist_refl (g z) (g z)); intros a b; rewrite (b (refl_equal (g z))); unfold Rgt in H; assumption. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet