proposition: Lemma exercise3_6b G B: sgraph G -> sub (range G) B -> sub (G \cg (complement_graph (inverse_graph G))) (complement_graph (diagonal B)).
proof: Proof. move=> gG srB; rewrite exercise3_6a // => t. move /compg_P => [pt [y /igraph_pP /setC_P [/setXp_P [pa pb] pc] pd]]. apply/setC_P; split; last by move /diagonal_i_P => [_ _ eq]; case: pc; ue. move:(@identity_sgraph B); rewrite - diagonal_is_identity => aux. apply /setX_i => //. apply/(domainP aux); exists(P t); apply /diagonal_pi_P; fprops. apply/(rangeP aux); exists(Q t);apply /diagonal_pi_P. split => //; apply: srB; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)