proposition: Lemma card_inj_ffuns D T : #|[set f : {ffun D -> T} | injectiveb f]| = #|T| ^_ #|D|.
proof: Proof. rewrite -card_inj_ffuns_on; apply: eq_card => f. by rewrite 2!inE; case: ffun_onP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)