proposition: Theorem Zmod_mod_mult : forall n a b, (0 < a)%Z -> (0 <= b)%Z -> Zmod (Zmod n (a * b)) b = Zmod n b.
proof: Proof. intros n a b Ha Hb. destruct (Zle_lt_or_eq _ _ Hb) as [H'b|H'b]. - rewrite (Z.mul_comm a b), Z.rem_mul_r, Z.add_mod, Z.mul_mod, Z.mod_same, Z.mul_0_l, Z.mod_0_l, Z.add_0_r, !Z.mod_mod; lia. - subst. now rewrite Z.mul_0_r, !Zmod_0_r. Qed.
imports: Coq(ZArith Lia Zquot)