proposition: Lemma subset_ball_prop_in_itvcc (R : realDomainType) (x : R) e P : 0 < e -> (ball_ Num.Def.normr x (2 * e) `<=` P)%classic -> {in `[(x - e), (x + e)], forall y, P y}.
proof: Proof. move=> e_gt0 PP y; rewrite in_itv/= -ler_distlC => ye; apply: PP => /=. by rewrite (le_lt_trans ye)// ltr_pMl// ltr1n. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed