proposition: Lemma insert_spec: forall L x, heapOrdered L -> Permutation (x :: L) (insert L x) /\ heapOrdered (insert L x).
proof: Proof. split. apply insert_permutation. apply insert_hO; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset