proposition: Lemma Cintegre : forall z z' : C, z <> zeroC -> Cmult z z' = zeroC -> z' = zeroC.
proof: Proof. intros. replace z' with (Cmult (Cmult (Cinv z) z) z') by (rewrite Cinv_l; trivial; ring). replace (Cmult (Cmult (Cinv z) z) z') with (Cmult (Cinv z) (Cmult z z')) by ring. rewrite H0; ring. Qed.