proposition: Lemma sub_pointxx (G : graph) (x:G) : sgraph.subgraph (sskeleton (point _ x x)) (skeleton G).
proof: Proof. apply: iso_subgraph; exact: iso_pointxx. 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)