proposition: Lemma l_2_1_2 : forall z1 z2 : CC, cc_IR (AbsCC (z1[*]z2) [^]2) [=] z1[*]z2[*]CC_conj z1[*]CC_conj z2.
proof: Proof. intros z1 z2. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (z1[*]z2[*]CC_conj (z1[*]z2)). Step_final (z1[*]z2[*] (CC_conj z1[*]CC_conj z2)). apply AbsCC_mult_conj. Qed.
imports: CoRN.complex.CComplex