proposition: Lemma stopsetE_help (s : {set 'I_n}) m0 n0 : n0 \in s -> m0 \in `F n0 -> #| s :&: `V m0 | != 1%nat -> exists n1, (m0 \in `F n1) /\ (n0 != n1) /\ (n1 \in s).
proof: Proof. move=> n0s m0n0 HwH. have : s :&: `V m0 :\ n0 != set0. move: HwH. apply contra. move/eqP. move/(f_equal (fun x => n0 |: x)). rewrite setD1K; last by rewrite inE n0s -FnextE. move=> ->. by rewrite cardsU1 /= cards0 inE. case/set0Pn => n1. rewrite in_setD1 => /andP [] n1n0. rewrite inE => /andP [] n1s1 m0n1. exists n1. rewrite FnextE m0n1; by rewrite eq_sym. 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