proposition: Lemma Ceq : forall z1 z2 : C, Cre z1 = Cre z2 /\ Cim z1 = Cim z2 <-> z1 = z2.
proof: Proof. intros z1 z2 ; split ; intro H. rewrite <- Cproj_right ; symmetry ; rewrite <- Cproj_right ; destruct H as (H, H0) ; rewrite H ; rewrite H0 ; reflexivity. split; rewrite H; reflexivity. Qed.
imports: Cdefinitions