proposition: Lemma unshift_interval_pred (i j:nat) : 0 < j -> unshift (interval (S i) j) = interval i (Nat.pred j).
proof: Proof. destruct j. inversion 1. intro; simpl. now rewrite unshift_interval. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)