proposition: Lemma can_imset_pre (T : finType) f g (A : {set T}) : cancel f g -> f @: A = g @^-1: A :> {set T}.
proof: Proof. move=> fK; apply: can2_imset_pre => // x. suffices fx: x \in codom f by rewrite -(f_iinv fx) fK. exact/(subset_cardP (card_codom (can_inj fK)))/subsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)