proposition: Lemma expF_mul a n m: exp_F a (n * m) = exp_F (exp_F a n) m.
proof: Proof. by elim: m; [ rewrite muln0 | move => m /= <-; rewrite expF_add mulnS ]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)