Natural ceilings of quotients

Main results

• Nat.ceil_div_eq_ceilDiv: real quotient ceilings equal natural ceiling division.
• Nat.le_ceilDiv_mul, Nat.ceilDiv_mul_lt: covering and overshoot bounds.

References

Adapted from Ceil.lean at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

The ceiling of a quotient of natural numbers

theorem Nat.ceilDiv_le_iff {a b k : ℕ} (hb : 0 < b) : a ⌈/⌉ b ≤ k ↔ a ≤ k * b

a ⌈/⌉ b ≤ k says that k pieces of size b cover a. Mathlib's ceilDiv_le_iff_le_mul has b * k on the right.

theorem Nat.le_ceilDiv_mul {a b : ℕ} (hb : 0 < b) : a ≤ a ⌈/⌉ b * b

a ⌈/⌉ b pieces of size b cover a.

theorem Nat.ceilDiv_mul_lt {a b : ℕ} (hb : 0 < b) : a ⌈/⌉ b * b < a + b

a ⌈/⌉ b pieces of size b overshoot a by less than one piece.

theorem Nat.ceil_div_eq_ceilDiv (a : ℕ) {b : ℕ} (hb : 0 < b) : ⌈↑a / ↑b⌉₊ = a ⌈/⌉ b

The ceiling of the real quotient of two natural numbers, in natural numbers.