proposition: Lemma cpo_order (x y : G) (p : Path i o) : x \in cp i o -> y \in cp i o -> irred p -> cpo x y = (idx p x <= idx p y).
proof: Proof. Proof using. move => /cpP cp_x /cpP cp_y Ip. rewrite /cpo. wlog suff Hyp : p Ip / x <[p] y -> forall q : Path i o, irred q -> ~ y <[q] x. { apply/idP/idP; rewrite leq_eqVlt; case/orP=> [/eqP|x_lt_y]. + by move=> /(idx_inj (cp_x the_uPath))->. + by rewrite leqNgt; apply/negP; apply: Hyp the_connect_irredP _ _ _. + by move=> /(idx_inj (cp_x p))->. + by rewrite leqNgt; apply/negP; apply: Hyp x_lt_y _ the_connect_irredP. } case/(three_way_split Ip (cp_x p) (cp_y p)) => [p1][_][p3][_ xNp3 yNp1]. move=> q Iq. case/(three_way_split Iq (cp_y q) (cp_x q)) => [q1][_][q3][_ yNq3 xNq1]. have := cp_x (pcat q1 p3); apply/negP. by rewrite mem_pcat negb_or; apply/andP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)