proposition: Lemma cols_starblank_mxProd : cols_starblank H (mxProd H y (mxStar H)) s.
proof: Proof. rewrite /cols_starblank => n1 n1s; apply/colP => m1. rewrite -[in RHS]cols_starblank_PCM_instance_erasures // 5!mxE. case: ifP => [m1n1|->//]. have -> : y ``_ n1 = Star. by move/subsetP : sy => /(_ _ n1s); rewrite inE => /eqP. rewrite Prod_cons_Star Prod_starblank_is_Star //. apply/allP => /= l /mapP[/= m0]. by rewrite mem_enum in_setD1 2!mxE => /andP[_ ->] ->. 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