proposition: Lemma last_take (A : Type) (p : seq A) t t1 j : j <= size p -> last t1 (take j p) = nth t (t1 :: p) j.
proof: Proof. elim: p t1 j => [t1 [|] //| a l IH t1 [|j]] //= H. by apply: IH. Qed.
imports: mathcomp(all_ssreflect)