proposition: Lemma heapsort_sorts: forall L, Permutation L (heapsort L) /\ Sorted Aleq (heapsort L).
proof: Proof. split. * intros. unfold heapsort. eapply Permutation_trans. apply heapify_permutation. apply heapsort_core_permutation. * apply heapsort_core_sorts. apply heapify_builds_heap. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset