proposition: Lemma adde_dst: forall e', evalid g e' -> dst UAdjMatGG_adde e' = dst g e'.
proof: Proof. intros. pose proof (edge_dst_snd g e'). pose proof (edge_dst_snd UAdjMatGG_adde e'). replace (dst g e') with (snd e') by trivial. replace (dst UAdjMatGG_adde e') with (snd 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