fact: Definition heapOrdered2 (L : list A) : Prop := forall i b, nth_error L i = Some b -> forall a, nth_error L (parent i) = Some a -> a <<= b.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset