Library prosa.util.div_mod

Require Export prosa.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

Definition div_floor (x y: nat) : nat := x %/ y.
Definition div_ceil (x y: nat) := if y %| x then x %/ y else (x %/ y).+1.

Lemma mod_elim:
  ∀ a b c,
    c>0 →
    b<c →
    (a + c - b)%%c = ( if a%%c ≥ b then (a%%c - b) else (a%%c + c - b)).