calc
  2 ^ k = 2 ^ 2 * 2 ^ (k - 2) := (pow_mul_pow_sub _ ?_).symm
  _ = 4 * 2 ^ (k - 2) := by norm_num
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ^ k = 4 * 2 ^ (k - 2)
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ≤ k