proposition: Lemma heapsort_core_sorts: forall L, heapOrdered L -> Sorted Aleq (heapsort_core L).
proof: Proof. intro L. apply heapsort_core_ind; clear L; intros. generalize (remove_min_spec _ H). rewrite e. intros [? ?]. subst. apply Sorted_nil. generalize (remove_min_spec _ H0). rewrite e. intros [? [? ?]]. constructor. apply H. trivial. destruct L'. rewrite heapsort_core_nil. apply HdRel_nil. rewrite heapsort_core_equation. generalize (remove_min_permutation (a0 :: L')). case remove_min. destruct o. 2: intros [? ?]; subst; discriminate. intros. apply HdRel_cons. rewrite Forall_forall in H2. apply H2. symmetry in H4. apply (Permutation_in _ H4). left. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset