proposition: Lemma HdRel_nth : forall l i n, Sorted lt l -> HdRel lt n l -> i < length l -> lt n (nth i l d).
proof: Proof. induction l; destruct i; simpl; intros. lia. lia. inversion H0. hyp. apply IHl. inversion H. hyp. destruct l. apply HdRel_nil. apply HdRel_cons. inversion H0. inversion H. inversion H8. subst. trans a; hyp. lia. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil) CoLoR(ListNodup) CoLoR(ListPermutation) Coq(Morphisms) CoLoR(NatUtil)