proposition: Theorem Sorted_merge_list_to_stack : forall stack l, SortedStack stack -> Sorted l -> SortedStack (merge_list_to_stack stack l).
proof: Proof. induction stack as [|[|]]; intros; simpl. - auto. - apply IHstack. + destruct H as (_,H1). fold SortedStack in H1. auto. + apply Sorted_merge; auto; destruct H; auto. - auto. Qed.
imports: List Setoid Permutation Sorted Orders