proposition: Lemma remove_min_hO: forall L, heapOrdered L -> match remove_min L with | (L', _) => heapOrdered L' end.
proof: Proof. intros. unfold remove_min. destruct L. apply heapOrdered_empty. generalize (foot_split_spec _ L). destruct (foot_split L). destruct o; intros; subst. rewrite app_comm_cons in H. apply heapOrdered_cutfoot in H. apply sink_hO. apply weak_heapOrdered_root with a. trivial. apply heapOrdered_empty. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset