ring_nf
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 + 1
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * (2 ^ (pn + 1) * 2) + k5 * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 2
no goals