proposition: Lemma all_starletter_iSP_BEC0S : forall l n0, all [pred i | starletter ((col n0 (iSP_BEC0 H (erase c E) l.+1)) i ord0) (c ``_ n0)] (enum ('F n0)).
proof: Proof. elim => [j|l IH j]. apply/allP => /= i ij. rewrite /starletter /= !mxE -mem_enum ij /Sum. case: ifPn => [_| K ]; first by apply/orP; left. apply/orP; right; apply/eqP; congr Bit. rewrite (sum_rowVnextD1_nostars Hc) //; last by rewrite -mem_enum. move=> n1. rewrite in_setD1 => /andP[n1j ijn1]. rewrite !mxE FnextE ijn1. case: ifPn => n1E; last first. rewrite Prod_colFnext_Bit //. apply/allP => m1. by rewrite mem_enum in_setD1 => /andP[xi xFn1] /=; rewrite !mxE xFn1. suff : false by []. move: K; rewrite -all_predC. move/allP => /= /(_ Star); apply. apply/mapP. exists n1 => //. by rewrite mem_enum in_setD1 n1j. by rewrite !mxE FnextE ijn1 n1E /colFnextD1 Prod_cons_Star Prod_mxStar_col_Star. apply/allP => i ij. rewrite /= mxE /starletter /= mxE -mem_enum ij. set starset := [set n1 | (n1 \in 'V i :\ j) && ((mxProd H (erase c E) (iSP_BEC0 H (erase c E) l.+1)) i n1 == Star) ]. have [/eqP H1|H1] : (#| starset | = O \/ 1 <= #| starset |)%nat. case: (#| starset| ); [tauto | move=> n0; by right]. - apply/orP; right. rewrite cards_eq0 in H1. have H0 : forall n0, n0 \in 'V i :\ j -> (mxProd H (erase c E) (iSP_BEC0 H (erase c E) l.+1)) i n0 = Bit c ``_ n0. move=> /= n0. rewrite in_setD1. case/andP => n0j n0i. have n0i' : i \in 'F n0 by rewrite FnextE. move: {n0i'}(starletter_mxProd_erase E n0i' (IH n0)). case/orP => [abs | /eqP //]. move/eqP/setP : H1 => /(_ n0). by rewrite in_set0 inE abs andbT in_setD1 n0j n0i. rewrite (sum_rowVnextD1_Bit Hc) //; first by rewrite -mem_enum. move=> *; by rewrite mxE H0. - move: H1. rewrite card_gt0 => /set0Pn[/= n1 Hn1]. apply/orP; left. rewrite /Sum ifT //. apply/hasP => /=; exists Star => //. move: Hn1; rewrite inE => /andP[]. rewrite in_setD1 => /andP[] n1j n1Vj /eqP <-. apply/mapP; exists n1 => //; rewrite ?mxE //. by rewrite mem_enum in_setD1 n1j. 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