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