proposition: Theorem last_grec1up (d : T) (n : nat) : size init <= n -> last d (grec1up n) = head d (gloop1 (n - size init).+1 (size init) a0 (rev init)).
proof: Proof. by move=> Hn; rewrite /grec1up /grec1down subSn // last_rev. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp