proposition: Lemma adj_edge_form: forall (g: UAdjMatGG) u v a b, adj_edge g (u,v) a b -> a <= b -> (u = a /\ v = b).
proof: Proof. intros. destruct H. assert (src g (u,v) <= dst g (u,v)). apply (undirected_edge_rep g). apply H. rewrite (edge_src_fst g), (edge_dst_snd g) in *. simpl in *. destruct H1. auto. destruct H1; subst u; subst v. lia. all: apply H. 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