exact Dvd.intro (2 * 5 ^ pn + t + k5) rfl
case intro
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
h5' : 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
no goals