proposition: Lemma eqlP : Equality.axiom eql.
proof: Proof. move=> a b; apply: (iffP idP) => [|<-]; last first. case: a => // a'; by rewrite /= eqxx. case: a b; [|by case|by case]. by move=> a'; case => //= b' /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode