proposition: Lemma interval_edges_sym (G : graph) (x y : G) : interval_edges x y = interval_edges y x.
proof: Proof. by rewrite /interval_edges interval_sym setUC. 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)