proposition: Theorem ZOmod_mod_mult : forall n a b, Z.rem (Z.rem n (a * b)) b = Z.rem n b.
proof: Proof. intros n a b. assert (Z.rem n (a * b) = n + - (Z.quot n (a * b) * a) * b)%Z. rewrite <- Zopp_mult_distr_l. rewrite <- Zmult_assoc. apply ZOmod_eq. rewrite H. apply Z_rem_plus. rewrite <- H. apply Zrem_sgn2. Qed.
imports: Coq(ZArith Lia Zquot)