proposition: Lemma Prod_erase_Star (c : 'rV['F_2]_n) (E : {set 'I_n}) m0 n0 (M : 'M[letter]_(m, n)): (forall j0, all [pred i | starletter ((col j0 M) i ord0) (c ``_ j0)] (enum (`F j0 :\ m0))) -> Prod (colFnextD1 H ((erase c E) ``_ n0) (col n0 M) n0 m0) = Star -> (forall i0, i0 \in `F n0 :\ m0 -> M i0 n0 = Star) /\ (erase c E) ``_ n0 = Star.
proof: Proof. move=> H1 H2. split. move=> m1 m1j0. rewrite in_setD1 in m1j0. case/andP : m1j0 => m1m0 m1j0. move: (H1 n0) => /allP/(_ m1); rewrite mem_enum in_setD1 m1j0 andbT m1m0 => /(_ isT). rewrite inE mxE /starletter; case/orP; first by move/eqP. move=> abs. move/eqP: H2; rewrite Prod_StarE => /forallP/(_ (bool_of_F2 (c ``_ n0))). have : N(Bit (~~ bool_of_F2 c ``_ n0) | colFnextD1 H ((erase c E) ``_ n0) (col n0 M) n0 m0) = O. apply/eqP. rewrite -notin_num_occ_0 inE negb_or /=. apply/andP; split. rewrite mxE. case: ifP => // j0E. by case/F2P : (c ``_ n0). apply/mapP. case=> /= m2 Hm2 H3. move: (H1 n0) => /allP/(_ _ Hm2) /=. rewrite mxE in H3. rewrite mxE -H3 /= => /eqP []. by case/F2P : (c ``_ n0). move=> ->. rewrite -notin_num_occ_0 inE negb_or. case/andP => H3 H4. case/mapP : H4. exists m1. by rewrite mem_enum 2!inE m1j0 m1m0. by rewrite mxE (eqP abs) bool_of_F2K. rewrite mxE. case: ifPn => // n0E. exfalso. move: H2; by rewrite mxE (negbTE n0E) Prod_colFnext_Bit. 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