proposition: Theorem last_rec2up k : last d (rec2up k.+1) = head d (loop2 k 2 a0 a1 [:: a1; a0]).
proof: Proof. by rewrite /rec2up /rec2down last_rev. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp