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.
From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
Additional lemmas about divn and modn.
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.
Definition div_ceil (x y : nat) := if y %| x then x %/ y else (x %/ y).+1.
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.
We show that for any two integers a and b,
a is less than a %/ b × b + b given that b is positive.
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.