Library Coq.ZArith.Zeuclid

From Coq.Classes Require Import Morphisms.
From Coq.ZArith Require Import BinInt.

Set Warnings "-deprecated-library-file".
From Coq.Numbers.Integer.Abstract Require Import 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)).

 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.