proposition: Lemma Q_mult_plus_is_dist : distributive Qmult_is_bin_fun Qplus_is_bin_fun.
proof: Proof. red in |- *. simpl in |- *. exact Qmult_plus_distr_r. Qed.
imports: CoRN.model.abgroups.Qabgroup CoRN.algebra.CRings CoRN.model.rings.Zring