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