unfold F
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (F n - 2) * F n = F (n + 1) - 2
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n + 1 - 2) * (2 ^ 2 ^ n + 1) = 2 ^ 2 ^ (n + 1) + 1 - 2