proposition: Lemma cpo_max x : x \in cp i o -> cpo x o.
proof: Proof. Proof using. move=> /cpP/(_ the_uPath) x_path. rewrite /cpo idx_end; [ exact: idx_mem | exact: the_connect_irredP ]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)