proposition: Lemma permutations_finite E: finite_set E -> permutations E = injections E E.
proof: Proof. move => h; set_extens t => /Zo_P [ha hb]. by move:(proj1 hb) => injf; apply:Zo_i. by apply:(permutation_if_inj h) hb; apply /functionsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)