case zero
m✝ m : ℕ
⊢ fib (m + zero + 1) = fib m * fib zero + fib (m + 1) * fib (zero + 1)

case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
m n : ℕ
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
induction' n with n ih generalizing m
no goals
case zero
m✝ m : ℕ
⊢ fib (m + zero + 1) = fib m * fib zero + fib (m + 1) * fib (zero + 1)
simp
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
intros
case succ
m✝ n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
specialize ih (m + 1)
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
case succ
m✝ n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
rw [add_assoc m 1 n, add_comm 1 n] at ih
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (succ n) + fib (m + 1) * (fib n + fib (n + 1))
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
simp only [fib_add_two, ih]
no goals
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (succ n) + fib (m + 1) * (fib n + fib (n + 1))
ring