exact Finset.single_le_sum (fun k _ ↦ Nat.zero_le (a.val k)) (Finset.mem_univ j)
case h₃
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j ≤ ∑ k : Fin (Nat.succ n), ↑a k
no goals