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