proposition: Theorem ZOdiv_mod_mult : forall n a b, (Z.quot (Z.rem n (a * b)) a) = Z.rem (Z.quot n a) b.
proof: Proof. intros n a b. destruct (Z.eq_dec a 0) as [Za|Za]. rewrite Za. now rewrite 2!Zquot_0_r, Zrem_0_l. assert (Z.rem n (a * b) = n + - (Z.quot (Z.quot n a) b * b) * a)%Z. rewrite (ZOmod_eq n (a * b)) at 1. rewrite Zquot_Zquot. ring. rewrite H. rewrite Z_quot_plus with (2 := Za). apply sym_eq. apply ZOmod_eq. rewrite <- H. apply Zrem_sgn2. Qed.
imports: Coq(ZArith Lia Zquot)