proposition: Lemma intvl_connected a b : connected (intvl a b).
proof: Proof. move=> x y Hx Hy z Hz; split. - exact: Rle_trans (proj1 Hx) (proj1 Hz). - exact: Rle_trans (proj2 Hz) (proj2 Hy). Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor