proposition: Lemma contains_all_cons : forall li l xi x, contains_all li l -> contains (I.convert xi) (Xreal x) -> contains_all (xi :: li) (x :: l).
proof: Proof. intros li l xi x [H1 H2] Hx. split. simpl. apply f_equal, H1. intros [|n]. exact Hx. apply H2. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog