proposition: Lemma sintervalP2 x y u : reflect ((exists2 p : Path u x, irred p & y \notin p) /\ (exists2 q : Path u y, irred q & x \notin q)) (u \in sinterval x y).
proof: Proof. Proof using. apply/(iffP idP). + rewrite !inE => /andP[/cpPn ? /cpPn ?] //. + case=>- [p] Ip yNp [q] Iq xNq. rewrite !inE. apply/andP;split; [exact: cpNI xNq|exact: cpNI yNp]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)