# Library prosa.util.div_mod

Section DivMod.

First, we show that if t1 / h is equal to t2 / h and t1 t2, then t1 mod h is bounded by t2 mod h.
Given two natural numbers x and y, the fact that x / y < (x + 1) / y implies that y divides x + 1.
Lemma ltdivn_dvdn :
x y,
x %/ y < (x + 1) %/ y
y %| (x + 1).
We prove an auxiliary lemma allowing us to change the order of operations _ + 1 and _ %% h.
x h,
h > 0
x %/ h = (x + 1) %/ h
(x + 1) %% h = x %% h + 1 .

We show that the fact that x / h = (x + y) / h implies that h is larder than x mod h + y mod h.
x y h,
h > 0
x %/ h = (x + y) %/ h
h > x %% h + y %% h.

End DivMod.

In this section, we define notions of div_floor and div_ceil and prove a few basic lemmas.
Section DivFloorCeil.

We define functions div_floor and div_ceil, which are divisions rounded down and up, respectively.
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.

We start with an observation that div_ceil 0 b is equal to 0 for any b.
Lemma div_ceil0:
b, div_ceil 0 b = 0.

Next, we show that, given two positive integers a and b, div_ceil a b is also positive.
Lemma div_ceil_gt0:
a b,
a > 0 b > 0
div_ceil a b > 0.

We show that div_ceil is monotone with respect to the first argument.
Given T and Δ such that Δ T > 0, we show that div_ceil Δ T is strictly greater than div_ceil (Δ - T) T.
We show that the division with ceiling by a constant T is a subadditive function.