proposition: Lemma lt_ereal_nbhs (R : realFieldType) (a b : \bar R) (r : R) : a < r%:E -> r%:E < b -> exists delta : {posnum R}, forall y, (`|y - r| < delta%:num)%R -> (a < y%:E) && (y%:E < b).
proof: Proof. move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb. - move: a b ltax ltxb; abstract: wlog. move=> {}a {}b ltxa ltxb. have m_gt0 : (Num.min ((r - a) / 2) ((b - r) / 2) > 0)%R. by rewrite lt_minr !divr_gt0 // ?subr_gt0. exists (PosNum m_gt0) => y //=; rewrite lt_minr !ltr_distl. move=> /andP[/andP[ay _] /andP[_ yb]]. rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=. rewrite -subr_gt0 opprD addrA {1}[(b - r)%R]splitr addrK. by rewrite divr_gt0 ?subr_gt0. by rewrite -subr_gt0 addrAC {1}[(r - a)%R]splitr addrK divr_gt0 ?subr_gt0. - have [//||d dP] := wlog a (r + 1)%R; rewrite ?lte_fin ?ltrDl //. by exists d => y /dP /andP[->] /= /lt_le_trans; apply; rewrite leey. - have [//||d dP] := wlog (r - 1)%R b; rewrite ?lte_fin ?gtrDl ?ltrN10 //. by exists d => y /dP /andP[_ ->] /=; rewrite ltNyr. - by exists 1%:pos%R => ? ?; rewrite ltNyr ltry. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed