proposition: Lemma wH0_inv v : wH v = O -> v = 0.
proof: Proof. move=> v0. apply/rowP => i; rewrite mxE; apply/eqP; move/eqP : v0; apply: contraTT => vi0. rewrite -lt0n -has_count; apply/hasP. exists (v ``_ i) => //; apply/mapP; exists i => //. by rewrite val_ord_tuple mem_enum. 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