no goals
m n : ℕ
⊢ gcd (fib m) (fib (n + 0 * m)) = gcd (fib m) (fib n)
simp
no goals
m n k : ℕ
⊢ gcd (fib m) (fib (n + (k + 1) * m)) = gcd (fib m) (fib n)
rw [←gcd_fib_add_mul_self m n k,
  add_mul,
  ← add_assoc,
  one_mul,
  gcd_fib_add_self _ _]