proposition: Lemma wH_castmx n (F : ringType) (x : 'rV[F]_n) n' (H : (1 = 1)%N * (n = n')) : wH (castmx H x) = wH x.
proof: Proof. case: H => H1 H2; subst n'. rewrite /wH !count_map /=; apply eq_in_count => /= i _. by rewrite castmxE /= !cast_ord_id. 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