proposition: Lemma EFin_expe r n : (r ^+ n)%:E = r%:E ^+ n.
proof: Proof. by elim: n => [//|n IHn]; rewrite exprS EFinM IHn expeS. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed