proposition: Lemma get_edge (G : graph) (U : {set G}) (x y : skeleton G) : x \in U -> y \in U -> x -- y -> exists e : edge G, e \in edge_set U.
proof: Proof. move => Hx Hy. rewrite /=/sk_rel => /andP[_]. case/existsP=> e He. exists e. move: He. by rewrite !inE => /orP[]/andP[/eqP-> /eqP->]; rewrite Hx Hy. 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)