proposition: Lemma first_point_of_divergence: forall l1 l2 (u: V), hd_error l1 = Some u -> hd_error l2 = Some u -> l1 <> l2 -> exists la v l1b l2b, l1 = la++v::l1b /\ l2 = la++v::l2b /\ hd_error l1b <> hd_error l2b.
proof: Proof. induction l1; intros. inversion H. destruct l2. inversion H0. simpl in H. inversion H. subst a. simpl in H0. inversion H0. subst v. clear H H0. destruct l1. destruct l2. contradiction. exists nil. exists u. exists nil. exists (v::l2). simpl. split. auto. split. auto. unfold not; intros; inversion H. destruct l2. exists nil. exists u. exists (v::l1). exists nil. simpl. split. auto. split. auto. unfold not; intros; inversion H. rename v into a. rename v0 into b. destruct (EV a b). ++ hnf in e. subst b. assert (a::l1 <> a::l2). unfold not; intros; rewrite H in H1; contradiction. apply (IHl1 (a::l2) a) in H; auto. destruct H as [la [x [l1b [l2b [? [? ?]]]]]]. exists (u::la). exists x. exists l1b. exists l2b. simpl. split. rewrite H; auto. split. rewrite H0; auto. auto. ++ exists nil. exists u. exists (a::l1). exists (b::l2). simpl. split. auto. split. auto. unfold complement, equiv in c. unfold not; intros. inversion H. contradiction. 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