fact: Fixpoint tuto_take n s {struct s} := match s, n with | x :: s', n'.+1 => x :: take n' s' | _, _ => [::] end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)