proposition: Lemma leq_take (s : seq T) k : size s <= n -> size (take k s) <= n.
proof: Proof. by move=> sn; rewrite size_take; case: ifPn => // ks; rewrite (leq_trans _ sn) // ltnW. Qed.
imports: mathcomp(all_ssreflect fingroup perm)