proposition: Lemma remove_min_spec: forall L, heapOrdered L -> match remove_min L with | (L', None) => L = L' /\ L' = nil | (L', Some a) => Permutation L (a :: L') /\ Forall (fun x => a <<= x) L' /\ heapOrdered L' end.
proof: Proof. intros. generalize (remove_min_hO L H), (remove_min_permutation L), (remove_min_min L H). case (remove_min L). destruct o; tauto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset