proposition: Lemma interval_edges_disj_cp (G : graph) (x y z : G) : z \in @cp G x y -> [disjoint interval_edges x z & interval_edges z y].
proof: Proof. move=> z_cpxy. rewrite -setI_eq0 -subset0. apply/subsetP => e. rewrite 6!inE negb_or !negb_and. case/andP=> /and3P[_ src_Ixz tgt_Ixz]. rewrite 5!inE negb_or !negb_and. case/and3P=> /andP[e_z _] src_Izy tgt_Izy. move: e_z. have : source e \in [set z] by rewrite -(intervalI_cp z_cpxy) inE src_Ixz src_Izy. rewrite inE =>->/=. have : target e \in [set z] by rewrite -(intervalI_cp z_cpxy) inE tgt_Ixz tgt_Izy. by rewrite inE =>->. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)