proposition: Lemma insert_hO: forall L x, heapOrdered L -> heapOrdered (insert L x).
proof: Proof. intros. unfold insert. apply swim_hO. apply weak_heapOrdered2_postpend. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset