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