proposition: Lemma add_edge_adj_edge2: forall (g: PGraph) e s t e' u v, e <> e' -> (adj_edge g e' u v <-> adj_edge (pregraph_add_edge g e s t) e' u v).
proof: Proof. intros; split; intros. + destruct H0. split. apply add_edge_preserves_strong_evalid; auto. rewrite add_edge_preserves_src; auto. rewrite add_edge_preserves_dst; auto. + destruct H0. apply add_edge_preserves_strong_evalid in H0; auto. split. apply H0. rewrite add_edge_preserves_src, add_edge_preserves_dst in H1; 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