proposition: Lemma exp_inj (k l : 'I_n) : (a ^+ k == a ^+ l) = (k == l).
proof: Proof. case H' : (k == l); first by rewrite (eqP H') eqxx. by move/negbT : H' => /exp_inj_helper_ord /negbTE. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming