proposition: Lemma Prod_filter_Star m n (A : 'M[letter]_(m, n)) n0 (s : {set 'I_m}) : Prod [seq A m0 n0 | m0 in s] = Prod [seq A m0 n0 | m0 <- enum s & A m0 n0 != Star].
proof: Proof. rewrite /Prod; case: ifPn => [H|]; do 2 rewrite (num_occ_map_filter [pred x | x != Star]) //. - by rewrite H. - rewrite -leqNgt leq_eqVlt => /orP[/eqP|] H; by [rewrite H ltnn | rewrite H ltnNge (ltnW H)]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode