proposition: Lemma real_ler_distl x y e : x - y \is real -> (`|x - y| <= e) = (y - e <= x <= y + e).
proof: Proof. by move=> Rxy; rewrite real_lter_norml // !lterBDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)