Library Coq.ZArith.Zeuclid


Require Import Morphisms BinInt ZDivEucl.
Local Open Scope Z_scope.

Definitions of division for binary integers, Euclid convention.

In this convention, the remainder is always positive. For other conventions, see Z.div and Z.quot in file BinIntDef. To avoid collision with the other divisions, we place this one under a module.

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)).

#[global]
 Instance mod_wd : Proper (eq==>eq==>eq) modulo.
#[global]
 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.