proposition: Lemma weak_heapOrdered_root: forall r1 L, heapOrdered (r1 :: L) -> forall r2, weak_heapOrdered (r2 :: L) root_idx.
proof: Proof. intros. apply weak_heapOrdered_bounded_root_weak_heapOrdered. apply heapOrdered_bounded_root_heapOrdered in H. apply weak_heapOrdered_bounded_root with r1. trivial. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset