proposition: Lemma nbh_finW c (P : forall x, nbh x -> Prop) : (forall e (h : 0 < e), P _ (@NFin R c e h)) -> forall (v : nbh c%:E), P _ v.
proof: Proof. move=> ih; move: {-2}c%:E (erefl c%:E). by move=> e eE v; case: v eE => // c' e' h [->]. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology