proposition: Lemma Z_mult_plus_is_dist : distributive Zmult_is_bin_fun Zplus_is_bin_fun.
proof: Proof. red in |- *. simpl in |- *. intros x y z. apply Zmult_plus_distr_r. Qed.
imports: CoRN.model.abgroups.Zabgroup CoRN.algebra.CRings