proposition: Lemma CP_tree_sinterval (U : {set G}) (x y : G) : is_tree (CP U) -> x \in CP U -> y \in CP U -> x ⋄ y -> [disjoint CP U & sinterval x y].
proof: Proof. Proof using G_conn. move => CP_tree x_cp y_cp xy. rewrite -setI_eq0 -subset0; apply/subsetP => u. rewrite inE [u \in set0]inE =>/andP[u_cp]. case/sintervalP2=> -[p] Ip yNp [q] Iq xNq. case: (CP_path u_cp x_cp Ip) => p_ [] Ip_ p_cp /subsetP/(_ y) p_p. case: (CP_path u_cp y_cp Iq) => q_ [] Iq_ q_cp /subsetP/(_ x) q_q. have {p Ip yNp p_p} yNp_ : y \notin p_ by exact: contraNN yNp. have {q Iq xNq q_q} xNq_ : x \notin q_ by exact: contraNN xNq. have Ip_xy : irred (pcat p_ (edgep xy)). { rewrite irred_cat Ip_ irred_edge. apply/eqP/setP=> z. rewrite inE in_set1 mem_edgep. apply/andP/eqP=> [[z_p]/orP[]/eqP//z_y|->]; last by rewrite path_end eqxx. exfalso. move: z_y z_p =>->. by apply/negP. } have eq_ : q_ = pcat p_ (edgep xy). { apply CP_tree =>//. split=>//. apply/subsetP=> z. rewrite mem_pcat mem_edgep. by case/or3P=> [/(subsetP p_cp)|/eqP->|/eqP->]. } apply: contraNT xNq_ => _. by rewrite eq_ (@mem_pcat link_graph) mem_edgep eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)