proposition: Lemma exercise3_6a G: sgraph G -> commutes_at complement_graph inverse_graph G.
proof: Proof. move => gG. have gc: sgraph (complement_graph G) by apply: complement_graph_g. rewrite /commutes_at/complement_graph (igraph_range gG)(igraph_domain gG). set_extens t. move /setC_P => [/setX_P [pt pa pb] pc]. apply /igraphP; split => //; apply/ setC_P;split; first by fprops. by move /igraph_pP; rewrite pt. move /igraphP => [px /setC_P [/setXp_P [pa pb] pc]]. apply/setC_P; rewrite - px; split; [ fprops | by move /igraph_pP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)