proposition: Lemma nth_map : forall {T U} d' n (f : T -> U) l d, nth n (map f l) d = match le_lt_dec (length l) n with left _ => d | right _ => f (nth n l d') end.
proof: Proof. intros T U d' n f l d. destruct le_lt_dec as [H|H]. - apply nth_overflow. now rewrite map_length. - 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