proposition: Lemma Z_mod_lt a b : b > 0 -> 0 <= a mod b < b.
proof: Proof. Proof (fun Hb => Z.mod_pos_bound a b (Z.gt_lt _ _ Hb)). Lemma Z_mod_neg a b : b < 0 -> b < a mod b <= 0. Proof (Z.mod_neg_bound a b). Lemma Z_div_mod_eq_full a b : a = b*(a/b) + (a mod b). Proof. now destruct (Z.eq_dec b 0) as [->|?]; [destruct a|apply Z.div_mod]. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms