proposition: Lemma sink_step: forall L i p lc, nth_error L i = Some p -> nth_error L (left_child i) = Some lc -> forall j, (match nth_error L (right_child i) with | None => j = left_child i /\ ~(p <<= lc) | Some rc => (j = left_child i /\ ~(rc <<= lc) /\ ~(p <<= lc)) \/ (j = right_child i /\ rc <<= lc /\ (~p <<= rc)) end) -> sink (exchange L i j, j) = sink (L, i).
proof: Proof. intros. rewrite (sink_equation (L, i)). unfold sink1. rewrite H, H0. revert H1. case nth_error; intros. case (a <<=? lc); intros. destruct H1 as [[? [? ?]] | [? [? ?]]]; subst j. case (p <<=? a); auto. contradiction. contradiction. case (p <<=? a); auto. contradiction. destruct H1 as [[? [? ?]] | [? [? ?]]]; subst j. case (p <<=? lc). contradiction. auto. contradiction. destruct H1. subst. case (p <<=? lc). contradiction. auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset