proposition: Lemma sortOK : forall m l, length l = m -> length (sort l) = m.
proof: Proof. intros m l Hl. assert (H := Permuted_iter_merge l nil). apply Permutation.Permutation_length in H. unfold flatten_stack in H. simpl in H. rewrite <- Hl. rewrite H. unfold sort. reflexivity. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms