proposition: Lemma add_edge_unique_adj_edge: forall (g: PGraph) e u v e', ~ connected g u v -> adj_edge (pregraph_add_edge g e u v) e' u v -> e' = e.
proof: Proof. intros. destruct H0. destruct H0. destruct (EE e e'). auto. unfold complement, equiv in c. exfalso. apply H. apply add_edge_evalid_rev in H0; auto. rewrite add_edge_preserves_src, add_edge_preserves_dst in H2, H1; auto. simpl in H2. apply adjacent_connected. exists e'. split. split; auto. 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