proposition: Theorem Sorted_merge_stack : forall stack, SortedStack stack -> Sorted (merge_stack stack).
proof: Proof. induction stack as [|[|]]; simpl; intros. - constructor; auto. - apply Sorted_merge; tauto. - auto. Qed.
imports: List Setoid Permutation Sorted Orders