proposition: Lemma edge_set_adj (G : graph2) (x y : G) : @edge_set _ _ G [set x; y] == set0 -> ~~ @adjacent _ _ G x y.
proof: Proof. apply: contraTN => /existsP[e]. rewrite !inE => He. apply/set0Pn. exists e. rewrite !inE. by case/orP: He => /andP[->->]; rewrite orbT. 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)