fact: Definition B {R : realType} (x e : R) := @NFin R x (eclamp e) (gt0_clamp e).
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology