proposition: Lemma stopsetU s1 s2 : stopset s1 -> stopset s2 -> stopset (s1 :|: s2).
proof: Proof. move=> /forallP Hs1 /forallP Hs2; apply/forallP => /= m0. have : forall p : nat, (p == O) || (2 <= p) -> p != 1%nat by case=> //; case. apply. have Hp : forall p, p != 1%nat -> (p == O) || (2 <= p) by case=> //; case. case/orP: {Hs1}(Hp _ (Hs1 m0)) => [|{Hp}Hs1]. case/orP: {Hs2 Hp}(Hp _ (Hs2 m0)). rewrite 2!cards_eq0 => /eqP Hs1 /eqP Hs2. by rewrite setIUl Hs1 Hs2 setU0 cards0 eqxx. move=> Hs1; rewrite cards_eq0 => /eqP Hs2; apply/orP; right. by rewrite setIUl Hs2 set0U. apply/orP; right. by rewrite setIUl cardsU -(addn0 2%N) -addnBA ?leq_add // subset_leq_card // subsetIr. 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