proposition: Lemma last_rec1up k : last d (rec1up k) = head d (loop1 k 1 a0 [:: a0]).
proof: Proof. by rewrite /rec1up /rec1down last_rev. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp