proposition: Lemma ereal_nbhs_nbhs (p : \bar R) (A : set (\bar R)) : ereal_nbhs p A -> ereal_nbhs p (ereal_nbhs^~ A).
proof: Proof. move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=. - move=> /nbhs_ballP[_/posnumP[e]] ballA. apply/nbhs_ballP; exists (e%:num / 2) => //= r per. apply/nbhs_ballP; exists (e%:num / 2) => //= x rex. apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym. - exists (M + 1)%R; split; first by rewrite realD. move=> -[x| _ |_] //=; last by exists M. rewrite lte_fin => M'x /=. apply/nbhs_ballP; exists 1%R => //= y x1y. apply MA; rewrite lte_fin. rewrite addrC -ltrBrDl in M'x. rewrite (lt_le_trans M'x) // lerBlDl addrC -lerBlDl. rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //. rewrite ltrBrDr in M'x. rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //. by rewrite /Order.comparable (ltW M'x) orbT. by rewrite comparabler0 realD. by rewrite num_real. - exists (M - 1)%R; split; first by rewrite realB. move=> -[x| _ |_] //=; last by exists M. rewrite lte_fin => M'x /=. apply/nbhs_ballP; exists 1%R => //= y x1y. apply MA; rewrite lte_fin. rewrite ltrBrDl in M'x. rewrite (le_lt_trans _ M'x) // addrC -lerBlDl. rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //. by rewrite num_real. rewrite addrC -ltrBrDr in M'x. rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //. by rewrite /Order.comparable (ltW M'x). by rewrite comparabler0 realB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal