proposition: Lemma at_right_semi_open_interval a lb : (lb < a) -> at_right lb (fun x : R => lb < x <= a).
proof: Proof. move => Hlba. rewrite /at_right /within /locally. pose epsilon := (a - lb). have Hepspos : 0 < epsilon by rewrite /epsilon; lra. pose eps := mkposreal epsilon Hepspos. exists (pos_div_2 eps) => y. by move/ball_to_lra; rewrite /= /epsilon; lra. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl