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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 20 = t * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 5
no goals