proposition: Lemma last_take (T : eqType) (x : T) n s : last x (take n s) = if n == 0 then x else if n <= size s then nth x s n.-1 else last x s.
proof: Proof. elim: n s => [|n ihn] [|y s] //= in x *; rewrite {}ihn ltnS; case: n => //=. by move=> n; case: ltnP => // n_lt; apply/set_nth_default. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin