proposition: Lemma contract_ereal_ball_fin_lt r r' (e : {posnum R}) : (r' < r)%R -> (contract r%:E - e%:num <= -1)%R -> ereal_ball r%:E e%:num r'%:E.
proof: Proof. move=> r'r reN1; rewrite /ereal_ball. rewrite gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin//. rewrite ltrBlDl addrC -ltrBlDl (le_lt_trans reN1) //. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. 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