proposition: Lemma nth_map_dflt (C : Type) (x0 : C) (f : C -> C) (n : nat) (s : seq C) : nth x0 (map f s) n = if size s <= n then x0 else f (nth x0 s n).
proof: Proof. case: (leqP (size s) n); last exact: nth_map. by move=> ?; rewrite nth_default // size_map. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2