proposition: Lemma Dx : forall (D:C -> Prop) (x0:C), D_in (fun x:C => x) (fun x:C => 1) D x0.
proof: Proof. unfold D_in in |- *; unfold Cdiv in |- *; intros; unfold limit1_in in |- *; unfold limit_in in |- *; intros; simpl in |- *; split with eps; split; auto. intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros; rewrite (Cinv_r (x - x0) (Cminus_eq_contra x x0 (sym_not_eq H3))); unfold C_dist in |- *; rewrite (Cminus_diag_eq _ _ (refl_equal _)). rewrite Cnorm_C0 ; assumption. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet