proposition: Lemma mul_expE m n p : mul_exp m n p = muln (expn m n) p.
proof: Proof. by elim: n => [|n IHn] in p *; rewrite ?mul1n //= expnS IHn mulE mulnCA mulnA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring