proposition: Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Z.pos_div_eucl a b).
proof: Proof. induction a as [a IH|a IH| ]; simpl; rewrite ?IH. - destruct (Z.pos_div_eucl a b) as (p,q); simpl; case Z.ltb_spec; reflexivity. - destruct (Z.pos_div_eucl a b) as (p,q); simpl; case Z.ltb_spec; reflexivity. - case Z.leb_spec; trivial. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms