proposition: Lemma Prod_starletter m n (A : 'M_(m, n)) n0 (b : 'F_2) (s : {set 'I_m}): all [pred i | starletter (A i n0) b] (enum s) -> (exists2 i, i \in s & A i n0 != Star) -> Prod [seq A i n0 | i <- enum s] = Bit b.
proof: Proof. move=> H0 IH. rewrite (Prod_filter_Star A n0 s). set tmp := [seq _ | _ <- _ & _]. rewrite (_ : tmp = nseq (size tmp) (Bit b)); last first. apply: all_pred1P. apply/allP => /= x0. case/mapP => /= m1 Hm1 x0m1. rewrite x0m1. rewrite mem_filter in Hm1. case/andP : Hm1 => m1star Hm1. move/allP : H0 => /(_ m1); rewrite mem_enum => H0. have /H0 : m1 \in s by move: Hm1; rewrite mem_enum. by rewrite /= /starletter (negbTE m1star). rewrite Prod_nseq_not_blank // /tmp size_map size_filter -lt0n -has_count. apply/hasP. case: IH => i H1 H2. exists i => //; by rewrite 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