proposition: Lemma nth_map' : forall {T1} x1 {T2} (f : T1 -> T2) n s, nth (f x1) (map f s) n = f (nth x1 s n).
proof: Proof. intros T1 x T2 f n s. case (ssrnat.leqP (size s) n) => Hs. rewrite 2?nth_default ?size_map //. now apply nth_map. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct