proposition: Lemma interval_sym x y : interval x y = interval y x.
proof: Proof. by rewrite /interval [[set x; y]]setUC sinterval_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)