proposition: Lemma Bit_col l b (bl : Bit b <=l l) (A : 'cV[letter]_m) (s : {set 'I_m}) : (forall i : 'I_m, Bit b <=l blank_to_star (A i ord0)) -> forall b' : 'F_2, Bit b' \in l :: [seq A m0 ord0 | m0 in s] -> b' = b.
proof: Proof. move=> Ha b'. rewrite in_cons => /orP [Hy|]. by move: bl; rewrite -(eqP Hy) lel_Bit => /eqP[]. move/mapP => [x Hx Hf]. by move: (Ha x); rewrite -Hf lel_Bit => /eqP[]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode