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