proposition: Lemma exp_inj_helper_nat k l : k < n -> k < l -> l < n -> a ^+ k != a ^+ l.
proof: Proof. case: k => [|k] kn kl ln; first by rewrite expr0 eq_sym H // kl. have /H : 0 < l - k.+1 < n. apply/andP; split; first by rewrite ltn_subRL addn0. rewrite -subSn; by [rewrite leq_subLR ltn_addl | rewrite (ltn_trans _ kl)]. apply: contra => /eqP /(congr1 (fun x => x * a ^- k.+1)). have /divff -> : a ^+ k.+1 != 0 by rewrite expf_neq0. by rewrite -expfB // => ->. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming