proposition: Lemma skel_sub (G : graph2) : sgraph.subgraph (skeleton G) (sskeleton G).
proof: Proof. exists id => //= x y H _. exact: subrelUl. 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)