proposition: Lemma weak_heapOrdered_bounded_root: forall r1 L b, heapOrdered_bounded (r1 :: L) b -> forall r2, weak_heapOrdered_bounded (r2 :: L) b root_idx.
proof: Proof. repeat intro. split; intros. specialize (H i a H0). destruct i. contradiction. specialize (H H2). apply H. intro. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset