proposition: Lemma cc_inv_abs : forall x : CC, AbsCC [--]x [=] AbsCC x.
proof: Proof. intros. unfold AbsCC in |- *. apply sqrt_wd. apply bin_op_wd_unfolded. Step_final ( [--] (Re x) [^]2). Step_final ( [--] (Im x) [^]2). Qed.
imports: CoRN.complex.CComplex