proposition: Lemma sskeleton_adjacent (G : graph) (i o : G) : adjacent i o -> diso G (sskeleton (point G i o)).
proof: Proof. move=> Aio. exists (bij_id: bij G (sskeleton (point G i o))) => /=. by move=>x y; rewrite {2}/edge_rel/= => ->. rewrite /is_dhom. apply sskelP. - move=> x y. by rewrite sg_sym. - rewrite /edge_rel/=/sk_rel => e ->. exact: adjacent_edge. - by rewrite /edge_rel/=/sk_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)