proposition: Lemma set1_is_stopset : stopset test_mat set1.
proof: Proof. rewrite /stopset. apply/forallP => /= m0. have : forall a : nat, 1 < a -> a != 1%nat by case=> //; case. apply. rewrite cardsltn1P. case: m0 => -[ ? | ]. apply/existsP; exists 1; apply/existsP; exists 0. by rewrite !inE eqxx /= /test_mat !VnextE !tanner_relE /= !mxE !eqxx. case => [ ? | ]. apply/existsP; exists 1; apply/existsP; exists 0. by rewrite !inE eqxx /= /test_mat !VnextE !tanner_relE /= !mxE !eqxx. case => [ ? | ]. apply/existsP; exists 1; apply/existsP; exists 0. by rewrite !inE eqxx /= /test_mat !VnextE !tanner_relE /= !mxE !eqxx. case => [ ? | [] //]. apply/existsP; exists 1; apply/existsP; exists 0. by rewrite !inE eqxx /= /test_mat !VnextE !tanner_relE /= !mxE !eqxx. 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