proposition: Lemma fin_numX x n : x \is a fin_num -> x ^+ n \is a fin_num.
proof: Proof. by elim: n x => // n ih x finx; rewrite expeS fin_numM// ih. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed