proposition: Lemma subset_ball_prop_in_itv (R : realDomainType) (x : R) e P : (ball_ Num.Def.normr x e `<=` P)%classic <-> {in `](x - e), (x + e)[, forall y, P y}.
proof: Proof. by split=> exP y /=; rewrite ?in_itv (ltr_distlC, =^~ltr_distlC); apply: exP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed