proposition: Lemma Zmult_rem_distr_l: forall a b c, Z.rem (c*a) (c*b) = c * (Z.rem a b).
proof: Proof. intros. zero_or_not c. rewrite (Z.mul_comm c b). zero_or_not b. rewrite (Z.mul_comm b c). apply Z.mul_rem_distr_l; auto. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms