proposition: Lemma size_take_leq T {s : seq T} m : (size (take m s) <= m)%nat.
proof: Proof. rewrite size_take. case: ifPn => //. by rewrite -leqNgt. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist