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

We show that for any two integers a and c, a is less than a %/ c × c + c given that c is positive.

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