proposition: Lemma indices_aux_Sorted : forall i acc, Sorted lt acc -> HdRel le i acc -> Sorted lt (indices_aux acc i).
proof: Proof. induction i; simpl; intros. hyp. apply IHi. destruct (eq_dec (f i) a). 2: hyp. apply Sorted_cons. hyp. destruct acc. apply HdRel_nil. apply HdRel_cons. inversion H0. lia. destruct (eq_dec (f i) a). apply HdRel_cons. refl. inversion H0. apply HdRel_nil. apply HdRel_cons. lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)