proposition: Lemma adjacentI (G : graph) (x y : G) (e : edge G) : e \in edges x y -> adjacent x y.
proof: Proof. move=> He. apply/existsP. exists e. by rewrite inE He. 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)