proposition: Lemma adde_src: forall e', evalid g e' -> src UAdjMatGG_adde e' = src g e'.
proof: Proof. intros. pose proof (edge_src_fst g e'). pose proof (edge_src_fst UAdjMatGG_adde e'). replace (src g e') with (fst e') by trivial. replace (src UAdjMatGG_adde e') with (fst e') by trivial. reflexivity. 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