proposition: Lemma nth_map_lt : forall {T U} d' n (f : T -> U) l d, (n < length l)%nat -> nth n (map f l) d = f (nth n l d').
proof: Proof. intros T U d' n f l d H. rewrite (nth_indep _ d (f d')). apply map_nth. now rewrite map_length. 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