proposition: Lemma sink1_inc: forall L j L' j', sink1 L j = (L', Some j') -> j < j' < length L'.
proof: Proof. unfold sink1. intros L j L' j'. case_eq (nth_error L j). 2: discriminate. case_eq (nth_error L (left_child j)). 2: discriminate. case_eq (nth_error L (right_child j)). do 6 intro. case (a <<=? a0). case (a1 <<=? a). discriminate. intros. inversion H2. rewrite exchange_length. split. apply right_child_inc. apply nth_error_Some; congruence. case (a1 <<=? a0). discriminate. inversion 3. rewrite exchange_length. split. apply left_child_inc. apply nth_error_Some; congruence. do 5 intro. case (a0 <<=? a). discriminate. inversion 2. rewrite exchange_length. split. apply left_child_inc. apply nth_error_Some. congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset