proposition: Lemma nth_rec1upS k : nth d (rec1up k.+1) k.+1 = F (nth d (rec1up k) k) k.+1.
proof: Proof. by rewrite !nth_rec1up_last !last_rev head_rec1downS. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp