proposition: Lemma inv_image_disjoint g : function g -> {compat (Vfi g) : x y / disjoint x y}.
proof: Proof. move=> fg x y dxy; rewrite /disjoint -iim_fun_setI2 //. by apply /set0_P => t /iim_fun_P [u]; rewrite dxy => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)