proposition: Lemma Dadd : forall (D:C -> Prop) (df dg f g:C -> C) (x0:C), D_in f df D x0 -> D_in g dg D x0 -> D_in (fun x:C => f x + g x) (fun x:C => df x + dg x) D x0.
proof: Proof. unfold D_in in |- *; intros; generalize (limit_plus (fun x:C => (f x - f x0) * / (x - x0)) (fun x:C => (g x - g x0) * / (x - x0)) (D_x D x0) ( df x0) (dg x0) x0 H H0); clear H H0; 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 x1 H2); clear H1; intro; rewrite (Cmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1; rewrite (Cmult_comm (g x1 - g x0) (/ (x1 - x0))) in H1; rewrite <- (Cmult_add_distr_l (/ (x1 - x0)) (f x1 - f x0) (g x1 - g x0)) in H1; rewrite (Cmult_comm (/ (x1 - x0)) (f x1 - f x0 + (g x1 - g x0))) in H1; cut (f x1 - f x0 + (g x1 - g x0) = f x1 + g x1 - (f x0 + g x0)). intro; rewrite H3 in H1; assumption. ring. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet