proposition: Lemma igraph_proof (G : graph) (x y : skeleton G) : consistent (interval x y) (interval_edges x y).
proof: Proof. move=> e. rewrite inE =>[b]. rewrite inE =>/andP [_ H]. rewrite /edge_set in_set in H. move: H=>/andP[? ?]. by case b. 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)