proposition: Lemma card_wH_supp x : #| wH_supp x |%N = wH x.
proof: Proof. rewrite cardE size_filter /wH count_map -enumT /=. apply eq_in_count => /= i _; by rewrite inE. 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