Library Stdlib.ZArith.Zeuclid



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

#[local]
Set Warnings "-deprecated-library-file".
From Stdlib.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)).

#[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.