proposition: Lemma nth_rec2upSS' k : nth d (rec2up k.+2) k.+2 = F (nth d (rec2up k) k) (nth d (rec2up k.+1) k.+1) k.+2.
proof: Proof. by rewrite /rec2up !nth_rev ?size_rec2down // !subnn nth_rec2downSS'. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp