proposition: Lemma cp_sub_interval x y : cp x y \subset interval x y.
proof: Proof. Proof using G_conn. apply/subsetP=> z z_cpxy. rewrite !in_setU !in_set1 inE -implyNb negb_or. apply/implyP=> /andP[zNx zNy]. apply/andP; split. - apply: contraNN zNx => /(cp_tightenR z_cpxy). by rewrite cpxx !inE eq_sym. - rewrite cp_sym in z_cpxy. apply: contraNN zNy => /(cp_tightenR z_cpxy). by rewrite cpxx !inE eq_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)