fact: Fixpoint lastn {T} n {n2} : (n2+n).-tuple T -> n.-tuple T := if n2 is _.+1 return (n2+n).-tuple T -> n.-tuple T then fun p => lastn _ (behead_tuple p) else fun p => p.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype seq fintype tuple)