proposition: Lemma take_subseq (T : eqType) n (s : seq T) : subseq (take n s) s.
proof: Proof. by rewrite -[X in subseq _ X](cat_take_drop n) prefix_subseq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin