proposition: Lemma ball_ereal_ball_fin_le r r' (e : {posnum R}) : let e' : R := (fine (expand (contract r%:E + e%:num)) - r)%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' r'e'r rr' re1; rewrite /ereal_ball. move: rr'; rewrite le_eqVlt => /predU1P[->|rr']; first by rewrite subrr normr0. rewrite /ball /= ltr0_norm ?subr_lt0// opprB in r'e'r. rewrite ltr0_norm ?subr_lt0 ?lt_contract ?lte_fin//. rewrite opprB; move: r'e'r. rewrite /e' -ltrBlDr opprK subrK -lte_fin fine_expand //. by rewrite lt_expandRL ?inE ?ltW// 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