proposition: Lemma sskeleton_add (G : graph) (x y : G) : sgraph.subgraph (sskeleton (igraph x y)) (sgraph.add_edge (sigraph G x y) istart iend).
proof: Proof. exists id => // u v uv _; move: u v uv. apply sskelP. - move=> u v. by rewrite sg_sym. - move=> e sNt. rewrite /edge_rel /= -!val_eqE /=. apply/orP; left. by rewrite /edge_rel/=/sk_rel/edge_rel/=/sk_rel sNt adjacent_edge. - by rewrite /edge_rel/= -!val_eqE /= !eqxx => ->. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)