proposition: Lemma swim_hO: forall L j, weak_heapOrdered2 L j -> heapOrdered (swim L j).
proof: Proof. intros L j. apply swim_ind; intros. generalize (swim1_hO L0 j0 H). rewrite e. trivial. generalize (swim1_hO L0 j0 H0). rewrite e. apply H. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset