proposition: Lemma expand_ereal_ball_pinfty {e : {posnum R}} r : (e%:num <= 1)%R -> expand (1 - e%:num)%R < r%:E -> ereal_ball +oo e%:num r%:E.
proof: Proof. move=> e1 er; rewrite /ereal_ball gtr0_norm ?subr_gt0; last first. by case/ltr_normlP : (contract_lt1 r). rewrite ltrBlDl addrC -ltrBlDl -[ltLHS]expandK ?lt_contract//. by rewrite inE ger0_norm ?lerBlDl ?lerDr // subr_ge0. 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