proposition: Lemma Sorted_alt {A} : forall (cmp : A -> A -> Prop) (aI : Inhabitant A), forall L, (forall x, In x L -> cmp x x) -> (forall x y z, cmp x y -> cmp y z -> cmp x z) -> Sorted cmp L -> forall i j, 0 <= i -> i <= j -> j < Zlength L -> cmp (Znth i L) (Znth j L).
proof: Proof. induction L; intros. rewrite Zlength_nil in H4. lia. inversion H1. subst l a0. assert (i = 0 \/ i > 0) by lia. destruct H5. subst i. rewrite Znth_0_cons. assert (j = 0 \/ j > 0) by lia. destruct H5. subst j. rewrite Znth_0_cons. apply H. left. trivial. change (a :: L) with ([a] ++ L). rewrite Znth_app2. rewrite Zlength_one. destruct L. rewrite Zlength_one in H4. lia. apply (H0 a a0). inversion H8. trivial. change a0 with (Znth 0 (a0 :: L)). apply IHL; auto; autorewrite with sublist in *; try lia. intros. apply H. right. trivial. rewrite Zlength_one. lia. change (a :: L) with ([a] ++ L). rewrite Znth_app2. 2: rewrite Zlength_one; lia. rewrite Zlength_one. rewrite Znth_app2. 2: rewrite Zlength_one; lia. rewrite Zlength_one. apply IHL; auto; try lia. 2: rewrite Zlength_cons in H4; lia. intros. apply H. right. trivial. 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