proposition: Lemma prefix_mon : (forall i, g i < g (S i)) -> (forall i, prefix i < prefix (S i)).
proof: Proof. intros hg i. unfold prefix. set (is := indices i0). set (n := length is). destruct (lt_dec (S i) n); destruct (lt_dec i n). apply Sorted_nth. class. apply indices_Sorted. hyp. hyp. lia. lia. assert (n=S i). lia. subst. rewrite H, Nat.sub_diag. ded (nth_In d l). destruct (In_indices_aux_elim H0). inversion H1. lia. assert (e : S i - n = S (i-n)). lia. rewrite e. apply Nat.add_lt_mono_l. apply hg. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)