Dividing repeatedly by a power

Facts about n / b ^ j for the stages of an argument that divides a quantity by b at each step.

Main results

• Nat.le_div_pow_of_mul_pow_le: lower bound on n / b ^ j when a * b ^ d ≤ n and j ≤ d.
• Nat.mul_div_pow_succ_le: b * (n / b ^ (j + 1)) ≤ n / b ^ j.

theorem Nat.le_div_pow_of_mul_pow_le {a b d j n : ℕ} (hb : 0 < b) (hj : j ≤ d) (h : a * b ^ d ≤ n) : a ≤ n / b ^ j

If a b ^ d ≤ n, then a ≤ n / b ^ j for every j ≤ d.

theorem Nat.mul_div_pow_succ_le (n b j : ℕ) : b * (n / b ^ (j + 1)) ≤ n / b ^ j

Dividing by one more power of b: b (n / b ^ (j + 1)) ≤ n / b ^ j.