proposition: Lemma Prod_nseq_not_blank n x : n != O -> x != Blank -> Prod (nseq n x) = x.
proof: Proof. elim: n x => //= n IH x _ xblank; rewrite /Prod /=. case/letterP : x xblank => //= _. - rewrite add0n add1n (_ : N(Bit 1 | _) = O) //. apply/eqP; rewrite -notin_num_occ_0; apply/nseqP; by case. - rewrite (_ : N(Bit 0 | _) = O) //. apply/eqP; rewrite -notin_num_occ_0; apply/nseqP; by case. - rewrite !add0n (_ : N(Bit 1 | _) = O); last first. apply/eqP; rewrite -notin_num_occ_0; apply/nseqP; by case. rewrite (_ : N(Bit 0 | _) = O) //. apply/eqP; rewrite -notin_num_occ_0; apply/nseqP; by case. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode