proposition: Lemma first_divergence_bubble_ugly: forall l1 l2 (u v: V), l1 <> l2 -> hd_error l1 = Some u -> hd_error l2 = Some u -> last_error l1 = Some v -> last_error l2 = Some v -> u <> v -> NoDup l1 -> NoDup l2 -> exists la x l1b l2b y l1c l2c, l1 = la++x::l1b++y::l1c /\ l2 = la++x::l2b++y::l2c /\ (forall u, In u l1b -> ~ In u l2b) /\ (forall u, In u l2b -> ~ In u l1b) /\ l1b <> l2b.
proof: Proof. intros. apply (first_point_of_divergence l1 l2 u) in H; auto. destruct H as [la [x [l1b [l2b [? [? ?]]]]]]. subst l1; subst l2. rewrite last_err_split2 in H2, H3. destruct l1b. destruct l2b. contradiction. inversion H2. subst x. rewrite last_error_cons in H3. apply last_error_In in H3. apply NoDup_app_r in H6. apply NoDup_cons_2 in H6. contradiction. unfold not; intros. inversion H. destruct l2b. inversion H3. subst x. apply NoDup_app_r in H5. apply NoDup_cons_2 in H5. rewrite last_error_cons in H2. apply last_error_In in H2. contradiction. unfold not; intros. inversion H. assert (In v (v1::l2b)). { rewrite last_error_cons in H3. apply last_error_In in H3. auto. unfold not; intros. inversion H. } apply (first_point_of_convergence_ugly (v0::l1b) (v1::l2b) v) in H. 2: auto. 2: { rewrite last_error_cons in H2. apply last_error_In in H2. auto. unfold not; intros. inversion H7. } destruct H as [l1b' [l2b' [y [l1c [l2c [? [? [? ?]]]]]]]]. rewrite H. rewrite H7. exists la. exists x. exists l1b'. exists l2b'. exists y. exists l1c. exists l2c. split. auto. split. auto. split; 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