proposition: Lemma but_last_iota_from : forall l i, but_last i (iota_from (S i) (S l)) = i::iota_from (S i) l.
proof: Proof. induction l; simpl. reflexivity. intros. repeat f_equal. simpl. specialize (IHl (S i)). simpl in IHl. injection IHl. intros. rewrite H. auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)