proposition: Lemma AbsCC_wd : forall x y : CC, x [=] y -> AbsCC x [=] AbsCC y.
proof: Proof. intros x y. elim x. intros x1 x2. elim y. intros y1 y2. simpl in |- *. unfold cc_eq in |- *. unfold AbsCC in |- *. simpl in |- *. intros. change (sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2) [=] sqrt (y1[^]2[+]y2[^]2) (cc_abs_aid _ y1 y2)) in |- *. elim H. clear H. intros. apply sqrt_wd. algebra. Qed.
imports: CoRN.complex.CComplex