proposition: Lemma iim_graph_P x r y: (inc y (inverse_image r x)) <-> (exists2 u, inc u x & inc (J y u) r).
proof: Proof. by apply: (iff_trans (dirim_P _ x y)); split; move => [u ux pr]; ex_tac; apply /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)