proposition: Lemma starFnext_iter_mxSumProd (Hc : syndrome H c = 0) l : starFnext H y (iSP_BEC0 H y l) = erasures (Esti H y (iSP_BEC0 H y l)).
proof: Proof. case: l => [|l]; [exact starFnext_mxStar | exact: starFnext_iter_mxSumProdS]. 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