Discharge of the hSub recurrence hypothesis

The bialternant development is stated over a recurrence for the guarded complete-homogeneous polynomials; HInsert.lean proves it, so the resolvent identity and the shifted forms hold unconditionally.

theorem RS.hSubRec (k : ℕ) : HSubRec k

The add-one-variable recurrence, discharging the hypothesis the bialternant development is stated over.

theorem RS.sum_fin_resolvent' {k : ℕ} {A : Finset (Fin k)} {j : Fin k} (hj : j ∉ A) (hcard : A.card + 1 = k) (m : ℕ) : ∑ r : Fin k, (-1) ^ ↑r * (eSub A ↑r * hSubZ (insert j A) (↑m - ↑↑r)) = MvPolynomial.X j ^ m

The guarded resolvent, unconditionally.