proposition: Lemma exp_inj_helper_ord (k l : 'I_n) : k != l -> a ^+ k != a ^+ l.
proof: Proof. rewrite neq_ltn => /orP H'. wlog : k l H' / k < l. case: (H') => H''; first by apply. rewrite eq_sym; apply => //; by apply/or_comm. move=> kl; by rewrite exp_inj_helper_nat. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming