proposition: Lemma Prod_colFnext_Bit (b : 'F_2) (c : 'cV[letter]_m) (s : {set 'I_m}) : all [pred i | starletter (c i ord0) b] (enum s) -> Prod (ColFnext (Bit b) c s) = Bit b.
proof: Proof. move=> /= H1. apply/Prod_cons. rewrite Prod1 //; split => //. set l := [seq _ | _ in _]. case/boolP : (Bit b \in l) => Hlst. - left. apply Prod_starletter. apply/allP => x xFn0m0. by move: H1 => /allP/(_ x) /(_ xFn0m0). case/mapP : Hlst => 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/(_ _ Hm1). rewrite /= /starletter -Hx. case/orP => // xBitb. exfalso. move: Hlst; rewrite /l => /mapP; apply. exists m1 => //. by rewrite -Hx (eqP xBitb). 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