proposition: Lemma igraphP r y: inc y (inverse_graph r) <-> (pairp y /\ inc (J (Q y)(P y)) r).
proof: Proof. split; first by case/Zo_P => yp pr; split => //; apply: (setX_pair yp). move => [py pr]; exact:(Zo_i (setX_i py (range_i pr) (domain_i pr)) pr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)