proposition: Lemma ball_to_lra a y eps : ball a eps y <-> a - eps < y < a + eps.
proof: Proof. split. - rewrite /ball /= /AbsRing_ball /abs /= /minus; move/Rabs_def2. by rewrite /plus /= /opp /=; lra. - move => Haeps. rewrite /ball /= /AbsRing_ball /abs /= /minus /= /plus /opp /= . rewrite /Rabs. case: Rcase_abs; lra. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp