Library Stdlib.ZArith.Zdiv_facts

From Stdlib Require Import BinInt Zdiv PreOmega Lia.
Local Open Scope Z_scope.

Module Z.

Lemma diveq_iff c a b :
  (b = 0 /\ c = 0 \/ c*b <= a < c*b + b \/ c*b + b < a <= c*b) <-> a/b = c.

Lemma mod_diveq_iff c a b :
  (b = 0 \/ c*b <= a < c*b + b \/ c*b + b < a <= c*b) <-> a mod b = a-b*c.

Definition mod_diveq c a b := proj1 (mod_diveq_iff c a b).

Definition diveq c a b := proj1 (diveq_iff c a b).

Lemma eq_mod_opp m x y : x mod -m = y mod -m <-> x mod m = y mod m.

Lemma eq_mod_abs m x y : x mod (Z.abs m) = y mod (Z.abs m) <-> x mod m = y mod m.
End Z.