proposition: Lemma CP_tree_paths (U : {set G}) (x y : G) (p : Path link_graph x y) : is_tree (CP U) -> p \subset CP U -> irred p -> {in CP U, p =i cp x y}.
proof: Proof. Proof using G_conn. move=> [CPU_tree _] p_cp Ip z z_cp. apply/idP/idP; last exact: link_path_cp. have [x_cp y_cp] : x \in CP U /\ y \in CP U. { split; apply: (subsetP p_cp); by rewrite ?path_begin ?path_end. } move=> z_p. apply: cpTI => q0 /(CP_path x_cp y_cp)[q] [Iq q_cp /subsetP q_sub]. apply: q_sub. by have -> : q = p by exact: CPU_tree. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)