proposition: Lemma wH_const_mx b : b != 0 -> wH (const_mx b) = n.
proof: Proof. move=> b0; rewrite wH_sum (eq_bigr (fun=> 1%nat)) //. - by rewrite sum_nat_const card_ord muln1. - by move=> ? _; rewrite mxE b0. 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