fact: CoInductive isplit z x y : Path x y -> Prop := ISplit (p1 : Path x z) (p2 : Path z y) : irred p1 -> irred p2 -> (forall k, k \in p1 -> k \in p2 -> k = z) -> isplit z (pcat p1 p2).
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)