proposition: Lemma Prod_cons_starletter m n (b : 'F_2) n0 (s : {set 'I_m}) (M : 'M[letter]_(m, n)): all [pred i | starletter (M i n0) b] (enum s) -> Prod (Bit b :: [seq M i n0 | i in s]) = Bit b.
proof: Proof. move=> /= H1. apply/Prod_cons. rewrite Prod1 //; split => //. set l := [seq _ | _ in _]. case/boolP : (Bit b \in l) => Hl. left. transitivity (Prod [seq M m0 n0 | m0 <- (enum s)]) => //. apply (Prod_starletter H1). case/mapP : Hl => m1 H2 H3. exists m1; rewrite -?H3 //; by rewrite mem_enum in H2. right. rewrite (_ : l = nseq (size l) Star); last first. apply/all_pred1P/allP => /= x. case/mapP => m1 Hm1 Hx. move: H1 => /allP H1. case/orP: (H1 _ Hm1) => [|abs]. by rewrite Hx. exfalso. move/negP : Hl; apply. apply/mapP; exists m1 => //. by rewrite (eqP abs). apply/Prod_starblank_is_Star; by rewrite all_nseq orbT. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode