proposition: Lemma calculate_norm : forall x y : IR, (x[+I*]y) [*]CC_conj (x[+I*]y) [=] cc_IR (x[^]2[+]y[^]2).
proof: Proof. intros. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; rational. Qed.
imports: CoRN.reals.NRootIR