proposition: Theorem nth_rec1up n k : nth d (rec1up n) k = if n < k then d else iteri k (fun i c => F c (i + 1)) a0.
proof: Proof. case: (ltnP n k) => H; first by rewrite nth_default // size_rec1up. rewrite (@nth_rec1up_indep d d n k k) //. by rewrite nth_rec1up_last last_rec1up head_loop1. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp