proposition: Lemma iso_pointxx (G : graph) (x : G) : diso (sskeleton (point _ x x)) (skeleton G).
proof: Proof. exists (bij_id : bij (sskeleton (point G x x)) (skeleton G)) => u v /=. - case/or3P => // /and3P[uNv /eqP eq1 /eqP eq2]; move: uNv; by rewrite eq1 eq2 eqxx. - by rewrite {2}/edge_rel/= => ->. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)