proposition: Lemma exercise4_7 G H K: sub ((H \cg G) \cap K) ((H \cap (K \cg (inverse_graph G))) \cg (G \cap ((inverse_graph H) \cg K))).
proof: Proof. move=> t /setI2_P [] /compg_P [tp [y JG JH]] tK. apply /compg_P;split =>// ;rewrite - tp in tK. by exists y; apply : setI2_i => //; apply/compg_P; split;fprops; aw; ex_tac; apply /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)