proposition: Lemma permutations_set0: (permutations emptyset) = singleton (identity emptyset).
proof: Proof. apply: set1_pr; first exact:(permutation_id emptyset). move => a /permutationsP [[[fa _] _] sa ta]. by apply: function_exten; aww; rewrite sa => t /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)