proposition: Lemma dvdn_pred_predX n e : (n.-1 %| (n ^ e).-1)%N.
proof: Proof. by rewrite predn_exp dvdn_mulr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)