proposition: Lemma contains_map_Xreal : forall xi x, contains_all xi x -> forall n, contains (I.convert (nth n xi I.nai)) (nth n (map Xreal x) Xnan).
proof: Proof. intros xi x [H1 H2] n. rewrite (nth_map 0). destruct le_lt_dec as [H|H]. rewrite -> nth_overflow. now rewrite I.nai_correct. now rewrite H1. 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