proposition: Lemma Zm_mult_assoc : (associative Zm_mult_op).
proof: Proof. unfold associative. intros x y z. simpl. unfold ZModeq; unfold Zm_mult. rewrite Zmult_assoc. apply Zmodeq_refl. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields