proposition: Lemma wH_card_supp u : wH u = #|supp u|%N.
proof: Proof. rewrite wH_sum /supp -sum1dep_card [in RHS]big_mkcond; by apply/eq_bigr. 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