proposition: Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) : let e' := (r - fine (expand (contract r%:E - e%:num)))%R in ball r e' r' -> (r' < r)%R -> (`|contract r%:E - (e)%:num| < 1)%R -> ereal_ball r%:E (e)%:num r'%:E.
proof: Proof. move=> e' re'r' rr' X; rewrite /ereal_ball. rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//. move: re'r'. rewrite /ball /= gtr0_norm // ?subr_gt0// /e'. rewrite -ltrBlDl addrAC subrr add0r ltrNl opprK -lte_fin. rewrite fine_expand // lt_expandLR ?inE ?ltW//. by rewrite ltrBlDl addrC -ltrBlDl. 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