proposition: Lemma card_permutations E: finite_set E -> cardinal (permutations E) = (factorial (cardinal E)).
proof: Proof. move=> fsE. have cE: natp (cardinal E) by fprops. rewrite (permutations_finite fsE). by rewrite (card_injections fsE fsE) (ffactnn cE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)