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