proposition: Lemma adde_partial_graph: forall (g': UAdjMatGG), is_partial_graph g g' -> evalid g' (u,v) -> is_partial_graph UAdjMatGG_adde g'.
proof: Proof. intros. destruct H as [? [? [? ?]]]. split. intros. simpl. apply H. auto. split. intros. rewrite adde_evalid_or in H4. destruct H4. apply H1; auto. subst e; auto. split. intros. rewrite adde_evalid_or in H4. destruct H4. rewrite <- H2. apply adde_src. auto. auto. rewrite adde_src in H5 by auto. simpl in H5; auto. subst e. rewrite (edge_src_fst g'). rewrite (edge_src_fst UAdjMatGG_adde); auto. intros. rewrite adde_evalid_or in H4. destruct H4. rewrite <- H3. apply adde_dst. auto. auto. rewrite adde_dst in H5 by auto. simpl in H5; auto. subst e. rewrite (edge_dst_snd g'), (edge_dst_snd UAdjMatGG_adde); auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph