proposition: Lemma ereal_ball_ninfty_oversize (e : {posnum R}) x : (2 < e%:num)%R -> ereal_ball -oo e%:num x.
proof: Proof. move=> e2; rewrite /ereal_ball /= (le_lt_trans _ e2) // -opprB normrN opprK. rewrite (le_trans (ler_normD _ _)) // normr1 -lerBrDr. by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1)%R // addrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed