rw [prepend_two, factor_ten_pow, hpk1, ht]
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t
⊢ 2 ^ pn.succ.succ ∣ prepend_two (2 ^ pn.succ * ↑pk)
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t
⊢ 2 ^ pn.succ.succ ∣ 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t)