proposition: Lemma iota_from_lt_not_In i j l : i < j -> ~ In i (iota_from j l).
proof: Proof. intros; generalize (iota_from_sorted_ge l j (S i) H ). intros; now apply sorted_ge_not_In. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)