case zero

⊢ coprime (fib zero) (fib (zero + 1))

case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib (succ n + 1))
n : ℕ
⊢ coprime (fib n) (fib (n + 1))
induction' n with n ih
no goals
case zero

⊢ coprime (fib zero) (fib (zero + 1))
simp
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n + fib (n + 1))
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib (succ n + 1))
rw [fib_add_two]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n)
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n + fib (n + 1))
simp only [coprime_add_self_right]
no goals
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n)
simp [coprime, ih.symm]