proposition: Lemma path_partition_checkpoint: forall (g: PGraph) {fg: FiniteGraph g} (l1 l2: list V) p a b, Permutation (l1++l2) (VList g) -> In a l1 -> In b l2 -> connected_by_path g p a b -> exists v1 v2, In v1 p /\ In v2 p /\ In v1 l1 /\ In v2 l2 /\ adjacent g v1 v2.
proof: Proof. intros. assert (exists l, fits_upath g l p). apply connected_exists_list_edges in H2; auto. destruct H3 as [l ?]. pose proof (path_partition_checkpoint' g l1 l2 p l a b H H0 H1 H2 H3). destruct H4 as [v1 [v2 [? [? [? [? ?]]]]]]. exists v1; exists v2. repeat split; auto. destruct H8 as [e [? ?]]. exists e; auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph