no goals
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, n / p ^ i = ∑ i in Ico 1 b, (k + (n - k)) / p ^ i
simp only [add_tsub_cancel_of_le hkn]
no goals
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, (k + (n - k)) / p ^ i =
    ∑ i in Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0)
simp only [Nat.add_div (pow_pos hp.pos _)]
no goals
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) =
    ∑ i in Ico 1 b, k / p ^ i + ∑ i in Ico 1 b, (n - k) / p ^ i +
      card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))
simp [sum_add_distrib, sum_boole]