let s : Finset (Fin n.succ) := (Finset.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 : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
⊢ ↑a k = 0
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
⊢ ↑a k = 0