simp only [(fun k ↦ Nat.eq_zero_of_le_zero (hf k)), Finset.sum_const_zero,
             Nat.zero_ne_one] at h₂
case h₁
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
hf : ∀ (j : Fin (Nat.succ n)), ↑a j ≤ 0
⊢ False
no goals