proposition: Lemma adde_partial_lgraph: forall (g': UAdjMatGG), is_partial_lgraph g g' -> evalid g' (u,v) -> w = elabel g' (u,v) -> is_partial_lgraph UAdjMatGG_adde g'.
proof: Proof. intros. split. apply adde_partial_graph. apply H. auto. split. unfold preserve_vlabel; intros. destruct vlabel. destruct vlabel. auto. unfold preserve_elabel; intros. destruct H. destruct H3. unfold preserve_elabel in H4. destruct (E_EqDec e (u,v)). unfold equiv in e0. subst e. rewrite adde_elabel_new. rewrite H1. auto. unfold complement, equiv in c. apply add_edge_evalid_rev in H2. rewrite adde_elabel_old. rewrite <- H4. all: 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