proposition: Lemma tuto_size_cat : forall s1 s2, size (s1 ++ s2) = size s1 + size s2.
proof: Proof. by move=> s1 s2; elim: s1 => //= x s1 ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)