proposition: Lemma nbhs_ereal_ninfty : (\forall x \near -oo%E, P x) <-> [/\ P -oo%E & \forall x \near -oo, P x%:E].
proof: Proof. split=> [|[Py]] [x [xr Px]]; last by exists x; split=> // -[y||]//; apply: Px. by split; [|exists x; split=> // y xy]; apply: Px. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule