proposition: Lemma largest_stopset_is_unique : is_unique largest_stopset (fun E' => E' \subset E /\ covered_by (stopset H) E E' /\ stopset H E').
proof: Proof. apply maxset_is_unique. exact: stopset0. exact: stopsetU. 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