proposition: Lemma add_edge_connected_through_bridge1: forall (g: PGraph) e u v a b, ~ evalid g e -> connected g a u -> connected g v b -> connected (pregraph_add_edge g e u v) a b.
proof: Proof. intros. assert (vvalid g u). apply (connected_vvalid g a u H0). assert (vvalid g v). apply (connected_vvalid g v b H1). apply (add_edge_connected g e u v) in H0; auto. apply (add_edge_connected g e u v) in H1; auto. destruct H0 as [x [? [? ?]]]. destruct H1 as [x0 [? [? ?]]]. exists (x++x0). split. apply valid_upath_app; auto. rewrite H5; rewrite H6. unfold adjacent_err. exists e. split. apply (add_edge_strong_evalid g e u v); auto. left. split. rewrite add_edge_src; auto. rewrite add_edge_dst; auto. split. apply hd_error_app; auto. apply last_err_app; 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