proposition: Lemma interval_unroll : forall i j:nat , (i < j)%nat -> interval i j = i :: interval (S i) j.
proof: Proof. intros. change (interval i j = (i :: nil) ++ interval (S i) j). replace (i::nil) with (interval i i). rewrite interval_app with i i j. reflexivity. auto with arith. auto with arith. unfold interval. replace (S i - i)%nat with 1. reflexivity. abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)