proposition: Lemma nth_grec1up_last (d : T) k : nth d (grec1up k) k = last d (grec1up k).
proof: Proof. by rewrite (last_nth d) size_grec1up. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp