proposition: Lemma sinterval_bounds x y : (x \in sinterval x y = false) * (y \in sinterval x y = false).
proof: Proof. by rewrite !inE !mem_cpl andbF. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)