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