proposition: Lemma adjacent_edge (G : graph) (e : edge G) : adjacent (source e) (target e).
proof: Proof. apply: (adjacentI e). by rewrite !inE. 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)