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