proposition: Lemma heapsort_core_permutation: forall L, Permutation L (heapsort_core L).
proof: Proof. intro L. apply heapsort_core_ind; clear L; intros. generalize (remove_min_permutation L). rewrite e. intros [? ?]. subst. constructor. generalize (remove_min_permutation L). rewrite e. intros. eapply Permutation_trans. apply H0. constructor. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset