proposition: Lemma three_way_split x y (p : Path x y) a b : irred p -> a \in p -> b \in p -> a <[p] b -> exists (p1 : Path x a) (p2 : Path a b) p3, [/\ p = pcat p1 (pcat p2 p3), a \notin p3 & b \notin p1].
proof: Proof. move => irr_p a_in_p b_in_p a_before_b. case/(isplitP irr_p) def_p : _ / (a_in_p) => [p1 p2' irr_p1 irr_p2' _]. subst p. case: (idx_nLR irr_p b_in_p) => // Y1 Y2. case/(isplitP irr_p2') def_p1' : _ / (tailW Y2) => [p2 p3 irr_p2 irr_p3 D2]. subst p2'. exists p1. exists p2. exists p3. split => //. have A: a != b. { apply: contraTN a_before_b => /eqP=>?. subst b. by rewrite ltnn. } apply: contraNN A => A. by rewrite [a]D2 // path_begin. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)