proposition: Lemma starFnext_mxStar : starFnext H y (mxStar H) = erasures (Esti H y (mxStar H)).
proof: Proof. apply/setP => /= n0; rewrite !inE !mxE. case: ifPn => n0E. rewrite /colFnext Prod_cons_Star Prod_mxStar_col_Star eqxx andTb. apply/forallP => m0. apply/implyP => m0n0; by rewrite mxE m0n0. rewrite /= /colFnext Prod_cons_starletter //. apply/allP => m0; by rewrite mem_enum inE 2!mxE => ->. 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