proposition: Lemma tuto_last_cat : forall x s1 s2, last x (s1 ++ s2) = last (last x s1) s2.
proof: Proof. by move=> x s1 s2; elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)