proposition: Lemma Zm_plus_associative : (associative Zm_plus_op).
proof: Proof. red. intros x y z. simpl. unfold ZModeq. unfold Zm_plus. rewrite Zplus_assoc. apply Zmodeq_refl. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields