n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))

n : ℕ
⊢ ∀ (b : Bool) (n' : ℕ),
    fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
n : ℕ
⊢ fastFibAux n = (fib n, fib (n + 1))
apply Nat.binaryRec _ (fun b n' ih => _) n
no goals
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))
simp [fastFibAux]
n : ℕ
b : Bool
⊢ ∀ (n' : ℕ), fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
n : ℕ
⊢ ∀ (b : Bool) (n' : ℕ),
    fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
intro b
n : ℕ
b : Bool
n' : ℕ
⊢ fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
n : ℕ
b : Bool
⊢ ∀ (n' : ℕ), fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
intro n'
n : ℕ
b : Bool
n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
n : ℕ
b : Bool
n' : ℕ
⊢ fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
intro ih
no goals
n : ℕ
b : Bool
n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
cases b <;>
      simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih,
        congr_arg Prod.snd ih, Prod.mk.inj_iff] <;>
      simp [bit, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]