proposition: Lemma cc_mult_abs : forall x y : CC, AbsCC (x[*]y) [=] AbsCC x[*]AbsCC y.
proof: Proof. intros x y. elim x. intros x1 x2. elim y. intros y1 y2. intros. unfold AbsCC in |- *. apply sqrt_mult_wd. simpl in |- *. rational. Qed.
imports: CoRN.complex.CComplex