Library prosa.util.div_mod

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

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

Lemma div_floor_add_g:
  ∀ a c,
    c > 0 →
    a < a %/ c × c + c.

Lemma div_ceil_subadditive:
  ∀ T,
    subadditive (div_ceil^~T).