proposition: Lemma AbsCC_ap_zero : forall x : CC, [0] [#] AbsCC x -> x [#] [0].
proof: Proof. intro. elim x. intros x1 x2. simpl in |- *. unfold AbsCC in |- *. unfold cc_ap in |- *. change ([0] [#] sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2) -> x1 [#] [0] or x2 [#] [0]) in |- *. intros H. cut (x1[^]2 [#] [0] or x2[^]2 [#] [0]). intro H0. elim H0; clear H0; intros. left. apply cring_mult_ap_zero with x1. astepl (x1[^]2). auto. right. apply cring_mult_ap_zero with x2. astepl (x2[^]2). auto. apply cg_add_ap_zero. astepl (sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2) [^]2). apply nexp_resp_ap_zero. apply ap_symmetric_unfolded. auto. Qed.
imports: CoRN.complex.CComplex