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