proposition: Lemma indices_Sorted : forall i, Sorted lt (indices i).
proof: Proof. intro i. apply indices_aux_Sorted. apply Sorted_nil. apply HdRel_nil. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)