proposition: Lemma subset_erasures_Esti : s \subset erasures (Esti H y (mxStar H)).
proof: Proof. apply/subsetP => /= n0 Hn0; rewrite inE. move/subsetP : sy => /(_ _ Hn0). rewrite inE !mxE /colFnext => /eqP ->. by rewrite Prod_cons_Star Prod_mxStar_col_Star. 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