# norm_num extension for Nat.fib#

This norm_num extension uses a strategy parallel to that of Nat.fastFib, but it instead produces proofs of what Nat.fib evaluates to.

Auxiliary definition for proveFib extension.

Equations
Instances For
theorem Mathlib.Meta.NormNum.isFibAux_two_mul {n : } {a : } {b : } {n' : } {a' : } {b' : } (H : ) (hn : 2 * n = n') (h1 : a * (2 * b - a) = a') (h2 : a * a + b * b = b') :
theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one {n : } {a : } {b : } {n' : } {a' : } {b' : } (H : ) (hn : 2 * n + 1 = n') (h1 : a * a + b * b = a') (h2 : b * (2 * a + b) = b') :
partial def Mathlib.Meta.NormNum.proveNatFibAux (en' : Q()) :
(ea' : Q()) × (eb' : Q()) × Q(Mathlib.Meta.NormNum.IsFibAux «$en'» «$ea'» «$eb'») theorem Mathlib.Meta.NormNum.isFibAux_two_mul_done {n : } {a : } {b : } {n' : } {a' : } (H : ) (hn : 2 * n = n') (h : a * (2 * b - a) = a') : Nat.fib n' = a' theorem Mathlib.Meta.NormNum.isFibAux_two_mul_add_one_done {n : } {a : } {b : } {n' : } {a' : } (H : ) (hn : 2 * n + 1 = n') (h : a * a + b * b = a') : Nat.fib n' = a' def Mathlib.Meta.NormNum.proveNatFib (en' : Q()) : (em : Q()) × Q(Nat.fib «$en'» = «\$em»)

Given the natural number literal ex, returns Nat.fib ex as a natural number literal and an equality proof. Panics if ex isn't a natural number literal.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Mathlib.Meta.NormNum.isNat_fib {x : } {nx : } {z : } :
Nat.fib nx = z

Evaluates the Nat.fib function.

Equations
• One or more equations did not get rendered due to their size.
Instances For