proposition: Lemma contract_ereal_ball_pinfty r (e : {posnum R}) : (1 < contract r%:E + e%:num)%R -> ereal_ball r%:E e%:num +oo.
proof: Proof. move=> re1; rewrite /ereal_ball; rewrite [contract +oo]/= ler0_norm; last first. by rewrite subr_le0; case/ler_normlP: (contract_le1 r%:E). by rewrite opprB ltrBlDl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed