proposition: Lemma Zmod_mult_plus_distr_r : forall n m p : Z, (n * (m + p)) %= (n * m + n * p).
proof: Proof. intros; ring_simplify; apply mod_eq_refl. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory