proposition: Lemma indices_aux_complete : forall i x acc, x < i -> f x = a -> In x (indices_aux acc i).
proof: Proof. induction i; simpl; intros. absurd (x<0); lia. destruct (lt_dec x i). apply IHi; hyp. assert (x=i). lia. subst x. destruct (eq_dec (f i) a). 2: cong. apply In_indices_aux_intro. simpl. auto. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)