proposition: Lemma Sylvester_mxE (i j : 'I_dS) : let S_ r k := r`_(j - k) *+ (k <= j) in Sylvester_mx i j = match split i with inl k => S_ p k | inr k => S_ q k end.
proof: Proof. move=> S_ /[1!mxE]; case: {i}(split i) => i /[!mxE]/=; by rewrite rVpoly_delta coefXnM ltnNge if_neg -mulrb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)