fact: Fixpoint build_heap_helper (L : list A) (n : nat) := let L' := sink (L, n) in match n with | 0 => L' | S n' => build_heap_helper L' n' end.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset