proposition: Lemma nth_wH_supp k n (F : ringType) (y : 'rV[F]_n.+1) : (k <= n.+1)%N -> wH y = k -> forall j : nat, (j < k)%N -> y ``_ (nth ord0 (enum (wH_supp y)) j) != 0.
proof: Proof. move=> kn yD j jk; rewrite mem_wH_supp -mem_enum; apply/mem_nth. by rewrite -cardE card_wH_supp yD. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext