proposition: Lemma swim_step: forall L i a b, 0 < i < length L -> nth_error L i = Some b -> nth_error L (parent i) = Some a -> b <<= a -> swim (exchange L i (parent i)) (parent i) = swim L i.
proof: Proof. intros. assert (parent i < i) by (apply parent_dec; unfold root_idx; lia). rewrite (swim_equation L i). unfold swim1. rewrite H0, H1. case_eq (i <=? root_idx); intro. { apply Nat.leb_le in H4. unfold root_idx in H4. lia. } case (b <<=? a); intro. 2: contradiction. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset