proposition: Lemma Zm_mult_plus_dist : (distributive Zm_mult_op Zm_plus_op).
proof: Proof. red; simpl. intros x y z. unfold ZModeq; unfold Zm_mult; unfold Zm_plus. rewrite <-Zmult_plus_distr_r. apply Zmodeq_refl. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields