proposition: Lemma card_preimset (T : finType) (f : T -> T) (A : {set T}) : injective f -> #|f @^-1: A| = #|A|.
proof: Proof. move=> injf; apply: on_card_preimset; apply: onW_bij. have ontof: _ \in codom f by apply/(subset_cardP (card_codom injf))/subsetP. by exists (fun x => iinv (ontof x)) => x; rewrite (f_iinv, iinv_f). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)