proposition: Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ (@ereal_ball R)).
proof: Proof. set diag := fun r => [set xy | ereal_ball xy.1 r xy.2]. rewrite predeq2E => x A; split. - rewrite {1}/nbhs /= /ereal_nbhs. case: x => [/= r [_/posnumP[e] reA]| [M [/= Mreal MA]]| [M [/= Mreal MA]]]. + pose e' : R := Num.min (contract r%:E - contract (r%:E - e%:num%:E))%R (contract (r%:E + e%:num%:E) - contract r%:E)%R. exists (diag e'); rewrite /diag. exists e' => //. rewrite /= /e' lt_minr; apply/andP; split. by rewrite subr_gt0 lt_contract lte_fin ltrBlDr ltrDl. by rewrite subr_gt0 lt_contract lte_fin ltrDl. case=> [r' /= re'r'| |]/=. * rewrite /ereal_ball in re'r'. have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E). apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //. rewrite ger0_norm ?subr_ge0// in re'r'. have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R. move: re'r'; rewrite /e' lt_minr => /andP[+ _]. rewrite /e' ltrBrDl addrC -ltrBrDl => /lt_le_trans. by apply; rewrite opprB addrCA subrr addr0. rewrite -lt_expandRL ?inE ?contract_le1 // !contractK lte_fin. rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT. rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0. by rewrite -lee_fin -le_contract. apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. by rewrite (@lt_trans _ _ 0%R) // subr_lt0 -lte_fin -lt_contract. rewrite ltrNl opprB. rewrite /e' in re'r'. have r're : (contract r'%:E < contract (r%:E + e%:num%:E))%R. move: re'r'; rewrite lt_minr => /andP[_]. by rewrite ltrBlDr subrK. rewrite ltrBlDr -lte_fin -(contractK (_ + r)%:E)%R. by rewrite addrC -(contractK r'%:E) // lt_expand ?inE ?contract_le1. * rewrite /ereal_ball [contract +oo]/=. rewrite lt_minr => /andP[re'1 re'2]. have [cr0|cr0] := lerP 0 (contract r%:E). move: re'2; rewrite ler0_norm; last first. by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E). rewrite opprB ltrBrDl addrCA subrr addr0 => h. exfalso. move: h; apply/negP; rewrite -leNgt. by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)). move: re'2; rewrite ler0_norm; last first. by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E). rewrite opprB ltrBrDl addrCA subrr addr0 => h. exfalso. move: h; apply/negP; rewrite -leNgt. by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)). * rewrite /ereal_ball [contract -oo]/=; rewrite opprK. rewrite lt_minr => /andP[re'1 _]. move: re'1. rewrite ger0_norm; last first. rewrite addrC -lerBlDl add0r. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. rewrite ltrD2l => h. exfalso. move: h; apply/negP; rewrite -leNgt -lerNl. by move: (contract_le1 (r%:E - e%:num%:E)); rewrite ler_norml => /andP[]. + exists (diag (1 - contract M%:E))%R; rewrite /diag. exists (1 - contract M%:E)%R => //=. by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm. case=> [r| |]/=. * rewrite /ereal_ball [_ +oo]/= => rM1. apply: MA; rewrite lte_fin. rewrite ger0_norm in rM1; last first. by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm. rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr in rM1. rewrite subr_gt0 in rM1. by rewrite -lte_fin -lt_contract. * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA. * rewrite /ereal_ball /= opprK => h {MA}. exfalso. move: h; apply/negP. rewrite -leNgt [in leRHS]ger0_norm // lerBlDr. rewrite -/(contract M%:E) addrC -lerBlDr opprD addrA subrr sub0r. by move: (contract_le1 M%:E); rewrite ler_norml => /andP[]. + exists (diag (1 + contract M%:E)%R); rewrite /diag. exists (1 + contract M%:E)%R => //=. rewrite -ltrBlDl sub0r. by move: (contract_lt1 M); rewrite ltr_norml => /andP[]. case=> [r| |]. * rewrite /ereal_ball => /= rM1. apply MA. rewrite lte_fin. rewrite ler0_norm in rM1; last first. rewrite lerBlDl addr0 ltW //. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. rewrite opprB opprK -ltrBlDl addrK in rM1. by rewrite -lte_fin -lt_contract. * rewrite /ereal_ball /= -opprD normrN => h {MA}. exfalso. move: h; apply/negP. rewrite -leNgt [in leRHS]ger0_norm// -lerBlDr addrAC. rewrite subrr add0r -/(contract M%:E). by rewrite (le_trans _ (ltW (contract_lt1 M))) // ler_norm. * rewrite /ereal_ball /= => _; exact: MA. - case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA]] //=. + by apply nbhs_fin_inbound with e => ? ?; exact/sEA/reA. + have [|] := boolP (e%:num <= 1)%R. by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/reA. by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/reA. + have [|] := boolP (e%:num <= 1)%R. by move/nbhs_oo_down_e1; apply => ? ?; exact/sEA/reA. by rewrite -ltNge => /nbhs_oo_down_1e; apply => ? ?; exact/sEA/reA. 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