proposition: Lemma prefix_complete : (forall i, i >= i0 -> f i = a -> exists j, i = i0 + g j) -> (forall i, f i = a -> exists j, i = prefix j).
proof: Proof. intros hg i e. set (is := indices i0). set (n := length is). assert (n <= i0). unfold n, is. apply indices_length. destruct (lt_ge_dec i i0). ded (indices_complete l e). destruct (In_nth d H0) as [j [h1 h2]]. exists j. unfold prefix. fold is. fold n. destruct (lt_dec j n). hyp. contr. destruct (hg _ g0 e) as [j hj]. exists (n+j). unfold prefix. fold is. fold n. destruct (lt_dec (n+j) n). lia. assert (s : n+j-n=j). lia. rewrite s. hyp. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)