proposition: Lemma can2_in_imset_pre : {in D, cancel f g} -> {on D, cancel g & f} -> f @: D = g @^-1: D.
proof: Proof. move=> fK gK; apply/setP=> y; rewrite inE. by apply/imsetP/idP=> [[x Ax ->] | Agy]; last exists (g y); rewrite ?(fK, gK). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)