proposition: Lemma Sorted_nth_S : forall l i, Sorted lt l -> i < length l -> S i < length l -> lt (nth i l d) (nth (S i) l d).
proof: Proof. induction l; destruct i; simpl; intros. lia. lia. inversion H. subst. destruct l. simpl in H1. lia. inversion H5. hyp. inversion H. apply IHl. hyp. lia. lia. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil) CoLoR(ListNodup) CoLoR(ListPermutation) Coq(Morphisms) CoLoR(NatUtil)