no goals
m n : ℕ
⊢ fib (gcd m n) = gcd (fib m) (fib n)
induction m, n using Nat.gcd.induction with
| H0 => simp
| H1 m n _ h' =>
  rw [← gcd_rec m n] at h'
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
no goals
case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = gcd (fib 0) (fib n✝)
simp
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd (n % m) m) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
rw [← gcd_rec m n] at h'
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib (n % m + n / m * m))
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
conv_rhs => rw [← mod_add_div' n m]
no goals
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib (n % m + n / m * m))
rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]