proposition: Lemma F_Rcontains : forall X x, X >: x -> F X >: f0 x.
proof: Proof. clear -F_contains. move => X x /F_contains. rewrite /f0 /Xbind. case: xf => //. by case I.convert. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound