Library Coq.ZArith.Zeuclid
Definitions of division for binary integers, Euclid convention.
Module ZEuclid.
Definition modulo a b := Z.modulo a (Z.abs b).
Definition div a b := (Z.sgn b) * (Z.div a (Z.abs b)).
Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Instance div_wd : Proper (eq==>eq==>eq) div.
Theorem div_mod a b : b<>0 -> a = b*(div a b) + modulo a b.
Lemma mod_always_pos a b : b<>0 -> 0 <= modulo a b < Z.abs b.
Lemma mod_bound_pos a b : 0<=a -> 0<b -> 0 <= modulo a b < b.
Include ZEuclidProp Z Z Z.
End ZEuclid.