proposition: Lemma empty_interval i j : (j < i)%nat -> interval i j = nil.
proof: Proof. unfold interval. intro H; replace (S j - i)%nat with 0. reflexivity. abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)