proposition: Lemma set2_is_not_stopset : ~~ stopset test_mat set2.
proof: Proof. rewrite /stopset. rewrite negb_forall. apply/existsP; exists 0. rewrite negbK. apply/cards1P. exists 1. apply/setP => /= i. rewrite !inE /test_mat /= !VnextE !tanner_relE /= mxE. case: i. case=> [? // | ]. case=> [? // | ]. case=> [? // | ]. by case. 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