proposition: Lemma interval_app (i j k:nat): (i <= j)%nat -> (j <= k)%nat -> interval i k = interval i j ++ interval (S j) k.
proof: Proof. unfold interval;intros. replace (S k - i)%nat with ((S j - i) + (S k - S j))%nat. - rewrite iota_from_plus;repeat f_equal; lia. - abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)