proposition: Lemma number_of_injections_spec E F: finite_set F -> E <=cc F -> cardinal (injections E F) = factorial (cardinal F) %/c factorial (cardinal F -c cardinal E).
proof: Proof. move => ha hb. have nN: natp (cardinal F) by apply /NatP. have mN: natp (cardinal E) by apply: (NS_le_nat hb nN). have hc: finite_set E by apply /NatP. by rewrite (card_injections hc ha) (ffact_factd nN mN hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)