Pa zero

lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :    ∀ i, f i = 0 := by  have h₃ := Pa_evenShitZero f g  rw [h] at h₃  change 0 = f 0 at h₃  intro i  have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by    induction iv    exact h₃.symm    rename_i iv hi    have hivi : iv < n.succ := lt_of_succ_lt hiv    have hi2 := hi hivi    have h1 := Pa_evenShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩    have h2 := Pa_evenShiftSnd f g ⟨iv, succ_lt_succ_iff.mp hiv⟩    rw [h] at h1 h2    simp only [Fin.succ_mk, Fin.castSucc_mk] at h1 h2    erw [hi2] at h2    change 0 = _ at h2    simp only [neg_zero, zero_sub, zero_eq_neg] at h2    rw [h2] at h1    exact right_eq_add.mp h1  exact hinduc i.val i.prop