proposition: Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : {pred rT}) : {on R, bijective f} -> #|f @^-1: R| = #|R|.
proof: Proof. case=> g fK gK; rewrite -(can2_in_imset_pre gK) // card_in_imset //. exact: can_in_inj gK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)