proposition: Lemma swim_done: forall L i a b, nth_error L i = Some b -> nth_error L (parent i) = Some a -> ~ b <<= a -> swim L i = L.
proof: Proof. intros. rewrite swim_equation. unfold swim1. rewrite H, H0. case (i <=? root_idx); auto. case (b <<=? a); intro; trivial. contradiction. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset