fast_fib_aux_eq — Mathlib

English

The two definitions coincide: fastFib(n) = fib(n).

Русский

У двух определений совпадают значения: fastFib(n) = fib(n).

LaTeX

$$fastFib(n) = fib(n)$$

Lean4

theorem fast_fib_aux_eq (n : ℕ) : fastFibAux n = (fib n, fib (n + 1)) :=
  by
  refine Nat.binaryRec ?_ ?_ n
  · simp [fastFibAux]
  ·
    rintro (_ | _) n' ih <;>
        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] <;>
      simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]

Похожие утверждения