proposition: Lemma exercise3_4b G: sgraph G -> ((inverse_graph G) \cg G = emptyset <-> G = emptyset).
proof: Proof. move=> gG; split => h; last by rewrite h; apply: (proj2 (exercise3_4a _)). apply /set0_P => x xG; empty_tac1 (J (P x) (P x)). move:(eq_ind_r (inc^~ G) xG (gG x xG)) => px. by apply/compg_pP; exists (Q x) => //; apply /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)