proposition: Lemma all_mxStar n0 : all [pred i | mxStar i n0 == Star] (enum ('F n0)).
proof: Proof. apply/allP => m0 Hm0; by rewrite inE mxStarE // -mem_enum. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode