proposition: Lemma open_itvcc_subset : open A -> A x -> \forall r \near 0^'+, `[x - r, x + r] `<=` A.
proof: Proof. move=> /[apply] -[] _/posnumP[r]. have -> : r%:num = 2 * (r%:num / 2) by rewrite mulrCA divff// mulr1. move/subset_ball_prop_in_itvcc => /= xrA; exists (r%:num / 2) => //= k. rewrite /= distrC subr0 set_itvcc => /ltr_normlW kr k0. move=> z /andP [xkz zxk]; apply: xrA => //; rewrite in_itv/=; apply/andP; split. by rewrite (le_trans _ xkz)// lerB// ltW. by rewrite (le_trans zxk)// lerD// ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule