proposition: Lemma ereal_ballN x y (e : {posnum R}) : ereal_ball (- x) e%:num (- y) -> ereal_ball x e%:num y.
proof: Proof. by rewrite /ereal_ball 2!contractN opprK -opprB normrN addrC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed