[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib n' = a'
[PROOFSTEP]
rw [← hn, fib_two_mul, H.1, H.2, ← h1]
[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib (n' + 1) = b'
[PROOFSTEP]
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib n' = a'
[PROOFSTEP]
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib (n' + 1) = b'
[PROOFSTEP]
rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]
