proposition: Theorem Z_div_mod a b : b > 0 -> let (q, r) := Z.div_eucl a b in a = b * q + r /\ 0 <= r < b.
proof: Proof. Z.swap_greater. intros Hb. assert (Hb' : b<>0) by (now destruct b). generalize (Z.div_eucl_eq a b Hb') (Z.mod_pos_bound a b Hb). unfold Z.modulo. destruct Z.div_eucl. auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms