proposition: Lemma contract_ereal_ball_fin_le r r' (e : {posnum R}) : (r <= r')%R -> (1 <= contract r%:E + e%:num)%R -> ereal_ball r%:E e%:num r'%:E.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{r'} _|rr' re1]; first exact: ereal_ball_center. rewrite /ereal_ball ltr0_norm; last by rewrite subr_lt0 lt_contract lte_fin. rewrite opprB ltrBlDl (lt_le_trans _ re1) //. by case/ltr_normlP : (contract_lt1 r'). 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