fact: Definition grandsOk (L : list A) (p : nat) (rt : nat) : Prop := p <> root_idx -> parent p >= rt -> forall gs bb, parent gs = p -> nth_error L gs = Some bb -> forall a, nth_error L (parent p) = Some a -> a <<= bb.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset