proposition: Lemma w2c2w: forall w, 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 -> cdata_to_wedge (wedge_to_cdata w) = w.
proof: Proof. unfold wedge_to_cdata; unfold cdata_to_wedge; intros. repeat rewrite Int.signed_repr by auto. destruct w; destruct p; simpl; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist