proposition: Lemma sinterval_sym x y : sinterval x y = sinterval y x.
proof: Proof. apply/setP => p. by rewrite !inE andbC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)