proposition: Lemma exercise3_3a G H: sgraph G -> sgraph H -> ( sub (domain H) (domain G) <-> sub H (H \cg ((inverse_graph G) \cg G))).
proof: Proof. move=> gG gH. split => h t ts. move: (gH _ ts) => Jt; rewrite - Jt in ts. have: (inc (P t) (domain G)) by apply: h; ex_tac. move /(domainP gG)=> [y JG]; apply /compg_P; split => //; ex_tac. by apply /compg_pP; ex_tac; apply/igraph_pP. move /(domainP gH): ts => [y JH]. move: (h _ JH) => /compg_pP [z /compg_pP [u q _] _]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)