Theorem: Nat.Arith₁.beta_unbeta_recSequence_zero (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
⊢ (unbeta (recSequence f g z v)).beta 0 = f v
Tactic:
simpa using beta_unbeta_recSequence_eq f g z v 0 (inv_iff_ne_zero.mp rfl)
State after:
no goals