proposition: Lemma isplitP z x y (p : Path x y) : irred p -> z \in p -> isplit z p.
proof: Proof. move => I in_p. case/psplitP : _ / in_p I => p1 p2 /irred_catE [*]. by constructor. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)