proposition: Lemma subset_sub_contains_0 x0 (X0 X : I.type) : contains (I.convert X0) x0 -> subset' (I.convert X0) (I.convert X) -> contains (I.convert (I.sub prec X X0)) (Xreal 0).
proof: Proof. move=> Hx0 Hsub. destruct x0 as [|x0]. rewrite I.sub_propagate_r //. now destruct (I.convert X0). replace (Xreal 0) with (Xreal x0 - Xreal x0)%XR. apply I.sub_correct with (2 := Hx0). now apply Hsub. apply (f_equal Xreal). now apply Rminus_diag_eq. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor