proposition: Lemma sink1_length: forall L j, match sink1 L j with | (L', None) | (L', Some _) => length L = length L' end.
proof: Proof. unfold sink1. intros. case (nth_error L j); trivial. case (nth_error L (left_child j)); trivial. case (nth_error L (right_child j)); intros. case (a <<=? a0). case (a1 <<=? a); trivial. rewrite exchange_length. trivial. case (a1 <<=? a0); trivial. rewrite exchange_length; trivial. case (a0 <<=? a); trivial. rewrite exchange_length; trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset