proposition: Lemma fermat_little_pred a p : prime p -> ~(p %| a) -> a ^ p.-1 = 1 %[mod p].
proof: Proof. move=> Pp pNDa. have a_gt0 : 0 < a by case: a pNDa. have aCp : coprime a p by rewrite coprime_sym prime_coprime //; apply/negP. have aE : (egcdn a p).1 * a = 1 %[mod p]. by case: egcdnP => //= km kn -> _; rewrite (eqP aCp) modnMDl. rewrite -[_^ _]muln1 -modnMmr -[in LHS]aE // modnMmr. rewrite mulnC -mulnA -expnS prednK ?prime_gt0 //. by rewrite -modnMmr fermat_little // modnMmr aE. Qed.
imports: mathcomp(all_ssreflect)