proposition: Lemma fin_num_abs x : (x \is a fin_num) = (`| x | < +oo)%E.
proof: Proof. by rewrite fin_numE; case: x => // r; rewrite real_ltry normr_real. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed