proposition: Lemma sorted_sorted': forall g l, sorted g l -> sorted' g l.
proof: Proof. intros. unfold sorted'. induction H. intros. rewrite Zlength_nil in H0. lia. intros. rewrite Zlength_cons, Zlength_nil in H0. lia. intros. destruct (Z.lt_trichotomy i 0). lia. destruct H3. subst i. rewrite Znth_0_cons. rewrite Znth_pos_cons by lia. destruct (Z.lt_trichotomy (j-1) 0). lia. destruct H3. rewrite H3. rewrite Znth_0_cons. auto. specialize IHsorted with 0 (j-1). rewrite Znth_0_cons in IHsorted. apply (Z.le_trans (elabel g x) (elabel g y)). auto. apply IHsorted. lia. rewrite Zlength_cons in H2. lia. rewrite (Znth_pos_cons i) by lia. rewrite (Znth_pos_cons j) by lia. apply IHsorted. lia. rewrite Zlength_cons in H2. 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