proposition: Lemma sink_done: forall L i a, nth_error L i = Some a -> (forall b, nth_error L (left_child i) = Some b -> a <<= b) -> (forall b, nth_error L (right_child i) = Some b -> a <<= b) -> sink (L, i) = L.
proof: Proof. intros. rewrite sink_equation. unfold sink1. rewrite H. case_eq (nth_error L (left_child i)); auto. intros. specialize (H0 _ H2). case_eq (nth_error L (right_child i)); intros. specialize (H1 _ H3). case (a1 <<=? a0); intro. case (a <<=? a1); auto. contradiction. case (a <<=? a0); auto. contradiction. case (a <<=? a0); auto. contradiction. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset