proposition: Lemma interval_interval_cap (x y u z: G) : u \in cp x y -> z \in interval x u -> z \in interval u y -> z = u.
proof: Proof. move => cp_u Z1 Z2. move: (intervalI_cp cp_u). move/setP/(_ z)/esym. by rewrite 2!inE Z1 Z2 => /eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)