proposition: Lemma indices_length : forall i, length (indices i) <= i.
proof: Proof. intro i. ded (indices_aux_length i nil). unfold indices. simpl in H. lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)