proposition: Lemma grandsOk_root: forall L j, grandsOk L j root_idx <-> (j <> root_idx -> forall jj bb, parent jj = j -> nth_error L jj = Some bb -> forall a, nth_error L (parent j) = Some a -> a <<= bb).
proof: Proof. split; repeat intro; eapply H; eauto. unfold root_idx. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset