Pa zero

lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :    ∀ i, f i = 0 := by  have h₃ := Pa_oddShiftShiftZero f g  rw [h] at h₃  change 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_oddShiftShiftSnd f g ⟨iv, hivi⟩    rw [h, hi2] at h1    change 0 = _ at h1    simp only [neg_zero, succ_eq_add_one, zero_sub, zero_eq_neg] at h1    have h2 := Pa_oddShiftShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩    simp only [succ_eq_add_one, h, Fin.succ_mk, Fin.castSucc_mk, h1, add_zero] at h2    exact h2.symm  exact hinduc i.val i.prop