proposition: Lemma remove_min_min: forall L, heapOrdered L -> match remove_min L with | (L', None) => L = L' /\ L' = nil | (L', Some a) => Forall (fun x => a <<= x) L' end.
proof: Proof. intro. generalize (remove_min_permutation L). generalize (remove_min_root L). case remove_min. destruct o; auto. intros. generalize (root_minimal _ H1 a H); intro. clear H H1. eapply forall_permutation in H2. 2: apply H0. apply Forall_inv_tail with a. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset