proposition: Lemma but_last_iota_from' j : forall i, but_last i (iota_from (S i) (S j)) = iota_from i (S j).
proof: Proof. intros; rewrite but_last_iota_from. reflexivity. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)