proposition: Lemma nonzero_produit : forall z z' : C, z <> zeroC -> z' <> zeroC -> Cmult z z' <> zeroC.
proof: Proof. intros. apply nonzero_module. rewrite Cmult_module. apply Rmult_integral_contrapositive. split; auto with geo. Qed.