proposition: Lemma intvl_lVu l u x0 x : intvl l u x -> intvl l u x0 -> intvl l x0 x \/ intvl x0 u x.
proof: Proof. move=> [H1 H2] [H3 H4]. have [Hle|Hlt] := Rle_lt_dec x x0. by left. by move/Rlt_le in Hlt; right. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor