proposition: Lemma nbh_pinfW (P : forall x, nbh x -> Prop) : (forall M, P _ (@NPInf R M)) -> forall (v : nbh +oo), P _ v.
proof: Proof. move=> ih; move: {-2}+oo%E (erefl (@EPInf R)). 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