proposition: Lemma Z_mult_div_bounds : forall a b, 0 < b -> a - b < b * (a / b) <= a.
proof: Proof. intros a b N; split. pose proof Z_mod_lt a b. rewrite Z_mult_div_mod; lia. apply Z_mult_div_ge; lia. Qed.
imports: ZArith Lia Znumtheory