proposition: Lemma Z_div_mod_POS : forall b:Z, b > 0 -> forall a:positive, let (q, r) := Z.pos_div_eucl a b in Zpos a = b * q + r /\ 0 <= r < b.
proof: Proof. intros b Hb a. Z.swap_greater. generalize (Z.pos_div_eucl_eq a b Hb) (Z.pos_div_eucl_bound a b Hb). destruct Z.pos_div_eucl. rewrite Z.mul_comm. auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms