proposition: Theorem nth_grec1up d n k : nth d (grec1up n) k = if n < k then d else if k < size init then nth d init k else G (iteri (k - size init) (fun i c => F c (i + size init).+1) a0) k.
proof: Proof. case: (ltnP n k) => H; first by rewrite nth_default // size_grec1up. rewrite (nth_grec1up_indep (d2 := d) (m2 := k)) //. case: (ltnP k (size init)) => H'; first by rewrite grec1up_init // nth_take. rewrite nth_grec1up_last last_grec1up // head_gloop1; congr G. by rewrite subnK. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp