proposition: Lemma interval_sorted_ge: forall p n q : nat, (q <= n)%nat -> sorted_ge q (interval n p).
proof: Proof. unfold interval; intros; now apply iota_from_sorted_ge. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)