proposition: Lemma g2wedgelist_repable: forall g w, In w (graph_to_wedgelist g) -> Int.min_signed <= fst w <= Int.max_signed /\ Int.min_signed <= fst (snd w) <= Int.max_signed /\ Int.min_signed <= snd (snd w) <= Int.max_signed.
proof: Proof. intros. unfold graph_to_wedgelist in H. apply list_in_map_inv in H. unfold edge_to_wedge in H. destruct H; destruct H. apply EList_evalid in H0. subst w; simpl. split. apply weight_valid; auto. rewrite <- (src_fst g), <- (dst_snd g) by auto. apply evalid_strong_evalid in H0. destruct H0. destruct H0. rewrite vertex_valid in H0, H1. set (i:=Int.min_signed); compute in i; subst i. split; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph