proposition: Lemma adjacentP (G : graph) (P : G -> G -> Prop) : Symmetric P -> (forall e : edge G, P (source e) (target e)) -> (forall x y : G, adjacent x y -> P x y).
proof: Proof. move=> S H x y. case/existsP=> e. rewrite !inE. case/orP=> /andP[/eqP<- /eqP<-] //. exact: S. 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)