proposition: Lemma sk_rel_sym (G : graph) : symmetric (@sk_rel G).
proof: Proof. move=> x y. by rewrite /sk_rel/= eq_sym adjacent_sym. 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)