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