proposition: Lemma eformat_adj': forall (g : UAdjMatGG) u v, evalid g (eformat (u,v)) -> adj_edge g (eformat (u,v)) u v.
proof: Proof. intros. split. apply (evalid_strong_evalid g); auto. destruct (Z.le_ge_cases u v). rewrite eformat1 in *. left. rewrite (edge_src_fst g), (edge_dst_snd g); auto. auto. auto. rewrite eformat2 in *. right. rewrite (edge_src_fst g), (edge_dst_snd g); auto. auto. 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