proposition: Lemma Prod_cons_Bit l b (bl : Bit b <=l l) (A : 'cV[letter]_m) (s : {set 'I_m}) : (forall i, Bit b <=l blank_to_star (A i ord0)) -> has is_Bit (l :: [seq A m0 ord0 | m0 in s]) -> Prod (l :: [seq A m0 ord0 | m0 in s]) = Bit b .
proof: Proof. move=> Ha. rewrite /Prod. set lst := l :: _ => Hb. case/boolP : (Bit 0 \in lst) => Hin0. case/boolP : (Bit 1 \in lst) => Hin1. move: (Bit_col bl Ha Hin0). by rewrite -(Bit_col bl Ha Hin1). move: Hin1; rewrite notin_num_occ_0 => /eqP ->. by rewrite -(Bit_col bl Ha Hin0) ltn0 lt0n -notin_num_occ_0 Hin0. move: (Hin0); rewrite notin_num_occ_0 => /eqP ->. case/boolP : (Bit 1 \in lst) => Hin1. by rewrite -(Bit_col bl Ha Hin1) ltn0 lt0n -notin_num_occ_0 Hin1. case/hasP : Hb. case/letterP => //; by [rewrite (negbTE Hin0) | rewrite (negbTE Hin1)]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode