proposition: Lemma heapsort_core_nil: heapsort_core nil = nil.
proof: Proof. rewrite heapsort_core_equation. reflexivity. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset