proposition: Lemma interval_not_empty_iff (n p : nat) : interval n p <> nil <-> (n <= p)%nat.
proof: Proof. split. - intro H; destruct (le_lt_dec n p); [trivial| ]. apply empty_interval in l. contradiction. - apply interval_not_empty. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)