proposition: Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z), {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.
proof: Proof. intros b Hb a. exists (Z.div_eucl a b). exact (Z_div_mod a b Hb). Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms