proposition: Lemma stopsetE (s : {set 'I_n}) : stopset s = [forall m0, [forall n0, (n0 \in s) && (m0 \in `F n0) ==> ((`V m0 :&: s) :\ n0 != set0)]].
proof: Proof. apply/idP/idP. move=> /forallP Hs; apply/'forall_forallP => m0 n0; apply/implyP => /andP[n0s m0n0]. case: (stopsetE_help n0s m0n0 (Hs m0)) => /= n1 [m0n1 [n0n1 n1s]]. apply/set0Pn. exists n1; by rewrite 2!inE eq_sym n0n1 in_setI -FnextE m0n1. move=> H0; apply/forallP => /= m0; apply/negP => abs. case/boolP : [exists n0, (n0 \in s) && (m0 \in `F n0)]; last first. move/negP; apply. have : #|[set n0 in s | n0 \in `V m0]| != O by rewrite (eqP abs). rewrite cards_eq0. case/set0Pn => n1. rewrite inE. case/andP => H1 H2. by apply/existsP; exists n1; rewrite FnextE H1. case/existsP => /= n0 /andP[n0W m0n0]. move/'forall_forallP : H0 => /(_ m0 n0); rewrite n0W m0n0 implyTb. case/set0Pn => /= n1. rewrite 3!inE. case/and3P => [n1n0 m0n1 n1W]. suff : 1 < #|[set n0 in s | n0 \in `V m0]| by rewrite (eqP abs). rewrite cardsltn1P. apply/existsP; exists n0; apply/existsP; exists n1. by rewrite eq_sym n1n0 andbT inE n0W /= andbC inE n1W /= m0n1 /= -FnextE. 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