proposition: Lemma exercise3_6d G: sgraph G -> ( G = (domain G) \times (range G) <-> G \cg ((complement_graph (inverse_graph G)) \cg G) = emptyset ).
proof: Proof. move=> gG; rewrite (exercise3_6a gG). transitivity (complement_graph G = emptyset). rewrite /complement_graph; split;first by move => <-; apply: setC_v. move => h; move:(empty_setC h) => aux; apply: extensionality => //. apply: (sub_graph_setX gG). split. move=> ->; rewrite igraph0. by move: (exercise3_4a G) => [-> ->]. move=> ce; apply /set0_P => x xK. move: (xK); move /setC_P => [] /setX_P [pa] /(domainP gG) [u J1G] /(rangeP gG) [v J2G] _. empty_tac1 (J v u); apply /compg_pP; ex_tac; apply /compg_pP; ex_tac. by apply/igraph_pP; rewrite pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)