proposition: Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) : ereal_loc_seq x @ \oo--> ereal_dnbhs x.
proof: Proof. move=> P; rewrite /ereal_loc_seq. case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first. have /ZnatP [N Nfloor] : floor (Num.max d 0%R) \is a Znat. by rewrite Znat_def floor_ge0 le_maxr lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin. have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx. by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat. have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat. by rewrite Znat_def floor_ge0 le_maxr lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl. have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx. by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat. have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat. by rewrite Znat_def floor_ge0. exists N => // n leNn; apply: dP; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0. rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0. rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r. by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor lerD// ler_nat. 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