proposition: Lemma fermat_little a p : prime p -> a ^ p = a %[mod p].
proof: Proof. move=> pP. elim: a => [|a IH]; first by rewrite exp0n // prime_gt0. by rewrite prime_modn_expSn // -addn1 -modnDml IH modnDml addn1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)