proposition: Lemma exp_int a b: (\F a) ^ (\F b) = \F (a ^b%N).
proof: Proof. by rewrite expx_nat; elim:b => // n h /=; rewrite h expnS mul_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)