proposition: Lemma sorted_wedge_le_flip_cmp_rel: forall L, Sorted (Basics.flip cmp_rel) L -> Sorted wedge_le (map heap_item_rep L).
proof: Proof. induction 1. constructor. simpl. constructor. apply IHSorted. inversion H0; constructor. red in H1. unfold heap_item_rep. red. red in H1. unfold cmp in H1. assert (Int.lt (fst b) (fst a) = false). { rewrite <- (negb_involutive (Int.lt _ _)). rewrite H1. trivial. } apply lt_false_inv in H3. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.floyd_ext.share CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel Sorting CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.kruskal.kruskal_specs