proposition: Lemma Dopp : forall (D:C -> Prop) (f df:C -> C) (x0:C), D_in f df D x0 -> D_in (fun x:C => - f x) (fun x:C => - df x) D x0.
proof: Proof. intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *; intros; generalize (H0 eps H1); clear H0; intro; elim H0; clear H0; intros; elim H0; clear H0; simpl in |- *; intros; split with x; split; auto. intros; generalize (H2 x1 H3); clear H2; intro ; repeat rewrite Cmult_opp_1_opp in H2 ; assumption. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet