proposition: Lemma expand_ereal_ball_fin_lt r' r (e : {posnum R}) : (r' < r)%R -> expand (contract r%:E - e%:num)%R < r'%:E -> (`|contract r%:E - e%:num| < 1)%R -> ereal_ball r%:E e%:num r'%:E.
proof: Proof. move=> r'r ? r'e'r. rewrite /ereal_ball gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin//. by rewrite ltrBlDl addrC -ltrBlDl -lt_expandLR ?inE ?ltW. 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