proposition: Lemma nth_cat s1 s2 n : nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).
proof: Proof. by elim: s1 n => [|x s1 IHs] []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)