proposition: Lemma mxProd_mxStar_PCM_instance (y : 'rV[letter]_n) : (forall n0, y ``_ n0 != Blank) -> mxProd H y (mxStar H) = PCM_instance y.
proof: Proof. move=> Hblank. rewrite /mxProd. apply/matrixP => i j; rewrite !mxE. case: ifP => /= ij; last by rewrite ij. rewrite /colFnextD1. case/orP : (letter_split (y ``_ j)) => [/existsP[x /eqP Hx]|]. rewrite Hx. apply Prod_colFnext_Bit => //; apply/allP => /= m1. by rewrite mem_enum in_setD1 !mxE => /andP[m1i ->]. move: (Hblank j). case/letterP : (y ``_ j) => // _ _. apply/Prod_starblank_is_Star/allP => /= y'. rewrite !inE => /orP[/eqP -> //| /mapP[x]]. by rewrite mxE mem_enum in_setD1 mxE => /andP[xi ->] ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) f2 ssr_ext ssralg_ext max_subset num_occ hamming ldpc_erasure tanner linearcode