proposition: Lemma inverse_direct_image f x: function f -> sub x (source f) -> sub x (Vfs (inverse_fun f) (Vfs f x)).
proof: Proof. move=> ff sxf t tx. apply/dirim_P; exists (Vf f t). by apply/Vf_image_P => //; ex_tac. rewrite ifun_g; apply/igraph_pP; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)