proposition: Lemma stopset0 : stopset set0.
proof: Proof. apply/forallP => /= m0; by rewrite set0I cards0. 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