proposition: Lemma Prod_map_not_Star m n (A : 'M_(m, n)) n0 (s : {set 'I_m}) : Prod [seq A m1 n0 | m1 in s] != Star -> exists b m1, m1 \in s /\ A m1 n0 = Bit b.
proof: Proof. rewrite Prod_StarE negb_forall => /existsP[b Hb]. case/boolP : (N(Bit (F2_of_bool (b : bool)) | [seq A m1 n0 | m1 in s]) == O) => [H0|]. have : 0 < N(Bit (F2_of_bool (~~ b)) | [seq A m1 n0 | m1 in s]). by rewrite lt0n; apply: contra Hb => /eqP ->. rewrite lt0n -notin_num_occ_0 negbK => /mapP[i Hi]. exists (F2_of_bool (~~ b)), i; by rewrite mem_enum in Hi. rewrite -notin_num_occ_0 negbK => /mapP[i Hi] H1. exists (F2_of_bool b), i; by rewrite mem_enum in Hi. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode