proposition: Theorem Sorted_iter_merge : forall stack l, SortedStack stack -> Sorted (iter_merge stack l).
proof: Proof. intros stack l H; induction l in stack, H |- *; simpl. - auto using Sorted_merge_stack. - assert (Sorted [a]) by constructor. auto using Sorted_merge_list_to_stack. Qed.
imports: List Setoid Permutation Sorted Orders