proposition: Lemma wH_opp v : wH (- v) = wH v.
proof: Proof. rewrite {1}/wH [X in tval X](_ : _ = [tuple of map (fun x => - x) (tuple_of_row v)]); last first. apply: eq_from_tnth => i /=; by rewrite !tnth_map mxE. rewrite count_map; apply eq_count => i /=; by rewrite oppr_eq0. 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