proposition: Lemma nth_rec2downSS' k : nth d (rec2down k.+2) 0 = F (nth d (rec2down k) 0) (nth d (rec2down k.+1) 0) k.+2.
proof: Proof. by rewrite !nth0 -[rec2down k]behead_rec2down head_rec2downSS. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp