proposition: Lemma at_right_le_at_point a b (Hab : a < b) : (filter_prod (at_right a) (at_point b) (fun x => x.1 <= x.2)).
proof: Proof. pose Q x := a < x < b. pose R x := x = b. apply: (Filter_prod _ _ _ Q R) => // . rewrite /at_right /within /locally. pose epsilon := (b - a). 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 /Q; rewrite /= /epsilon; lra. move => x y . rewrite /Q /R /=. lra. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl