proposition: Lemma starletter_mxProd_erase (c : 'rV['F_2]_n) (E : {set 'I_n}) (M : 'M_(m, n)) m0 n0 (m0n0 : m0 \in `F n0) : all [pred i | starletter ((col n0 M) i ord0) (c ``_ n0)] (enum (`F n0)) -> starletter ((mxProd H (erase c E) M) m0 n0) (c ``_ n0).
proof: Proof. move=> /= IH. rewrite mxE m0n0 /colFnextD1 mxE. case: ifP => n0E; last first. apply/orP; right. apply/eqP/Prod_cons_starletter/allP => i. rewrite mem_enum in_setD1 => /andP[_]; rewrite -mem_enum => iFn0. by move/allP : IH => /(_ _ iFn0) /=; rewrite mxE. rewrite Prod_cons_Star. set l := [seq _ | _ in _]. case/boolP : (Bit c ``_ n0 \in l) => Hl. apply/orP; right. rewrite (@Prod_starletter _ _ _ _ (c ``_ n0)) //. apply/allP => x; rewrite mem_enum in_setD1 => /andP[? x2]. by move/allP : IH => /(_ x); rewrite mem_enum => /(_ x2) /=; rewrite mxE. case/mapP : Hl => m1 Hm1 xm1. exists m1 => //. by rewrite mem_enum in Hm1. by rewrite -xm1. apply/orP; left. apply/eqP/Prod_starblank_is_Star/allP => /= y. case/mapP => /= m1; rewrite mem_enum in_setD1 => /andP[m1m0 Hm1] ->{y}. move/allP : IH => /(_ m1); rewrite mem_enum => /(_ Hm1) /=. rewrite mxE; case/orP => [/eqP -> //| /eqP abs]. rewrite abs. exfalso. move/negP : Hl; apply. apply/mapP; exists m1 => //. by rewrite mem_enum in_setD1 m1m0. by rewrite 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