proposition: Lemma cols_starblank_PCM_instance_erasures : cols_starblank H (PCM_instance H y) s.
proof: Proof. move=> n0 n0s; apply/colP => m1; rewrite !mxE; case: ifPn => // m1n0. by move/subsetP : sy => /(_ _ n0s); rewrite inE => /eqP. 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