proposition: Lemma Prod_starblank_is_Star s : all starblank s -> Prod s = Star.
proof: Proof. move=> K. rewrite /Prod. suff : forall x : 'F_2, N(Bit x | s) = O by move=> X; rewrite 2!X. move=> x. apply/eqP; rewrite -notin_num_occ_0. move/allP : K => /(_ (Bit x))/contra; exact. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode