proposition: Lemma nth_rec2up_last k : nth d (rec2up k) k = last d (rec2up k).
proof: Proof. by case: k => [//|k]; rewrite (last_nth d) size_rec2up. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp