no goals
α : Type u
β : Type ?u.218631
a b n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i =
    ∑ i in range n, a / b ^ (i + 1) * b + a * b - (∑ i in range n, a / b ^ i + a / b ^ n)
rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
Nat.div_one]
α : Type u
β : Type ?u.218631
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i
α : Type u
β : Type ?u.218631
a b n : ℕ
⊢ ∑ i in range n, a / b ^ (i + 1) * b + a * b - (∑ i in range n, a / b ^ i + a / b ^ n) ≤
    ∑ i in range n, a / b ^ i + a * b - (∑ i in range n, a / b ^ i + a / b ^ n)
refine' tsub_le_tsub_right (add_le_add_right (sum_le_sum fun i _ => _) _) _
α : Type u
β : Type ?u.218631
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / (b ^ i * b) * b ≤ a / b ^ i
α : Type u
β : Type ?u.218631
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i
rw [pow_succ', mul_comm b]
α : Type u
β : Type ?u.218631
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
α : Type u
β : Type ?u.218631
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / (b ^ i * b) * b ≤ a / b ^ i
rw [← Nat.div_div_eq_div_mul]
no goals
α : Type u
β : Type ?u.218631
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
exact Nat.div_mul_le_self _ _