# Library prosa.util.div_mod

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

# Additional Lemmas about divn and modn

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.
Lemma eqdivn_leqmodn :
∀ t1 t2 h,
t1 ≤ t2 →
t1 %/ h = t2 %/ h →
t1 %% h ≤ t2 %% 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.
Lemma addn1_modn_commute :
∀ 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.
Lemma addmod_le_mod :
∀ x y h,
h > 0 →
x %/ h = (x + y) %/ h →
h > x %% h + y %% h.
We prove that if x lies in an interval `[kT, (k+1)T)`, then x %/ T is equal to k.
Lemma divn_leq :
∀ k T x,
k × T ≤ x < k.+1 × T →
x %/ T = k.

# Floors and Ceilings of Fractions

We define notions of div_floor and div_ceil and prove a few basic lemmas.
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.
Lemma div_ceil_monotone1 :
∀ d m n,
m ≤ n → div_ceil m d ≤ div_ceil n d.
Given T and Δ such that Δ ≥ T > 0, we show that div_ceil Δ T is strictly greater than div_ceil (Δ - T) T.
Lemma leq_div_ceil_add1 :
∀ Δ T,
T > 0 → Δ ≥ T →
div_ceil (Δ - T) T < div_ceil Δ T.
We show that the division with ceiling by a constant T is a subadditive function.
Lemma div_ceil_subadditive :
∀ T, subadditive (div_ceil^~T).
We observe that when dividing a value exceeding T × n, then the ceiling exceeds n.
Lemma div_ceil_multiple :
∀ Δ T n,
T > 0 →
(T × n) < Δ →
n < div_ceil Δ T.
We show that for any two integers a and b, a is less than a %/ b × b + b given that b is positive.
Lemma div_floor_add_g :
∀ a b,
b > 0 →
a < a %/ b × b + b.
We prove a technical lemma stating that for any three integers a, b, c such that c > b, mod can be swapped with subtraction in the expression (a + c - b) %% c.
Lemma mod_elim :
∀ a b c,
c > b →
(a + c - b) %% c = if a %% c ≥ b then (a %% c - b) else (a %% c + c - b).