proposition: Lemma wH_rVpoly u : wH u = count (fun i : 'I_n => (rVpoly u)`_i != 0) (enum 'I_n).
proof: Proof. rewrite /wH count_map; apply eq_in_count => /= i _. rewrite coef_poly insubT // => ni. rewrite ltn_ord; congr (u _ _ != _); by apply val_inj. 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