proposition: Lemma heapOrdered_cutfoot: forall L a, heapOrdered (L ++ (a :: nil)) -> heapOrdered L.
proof: Proof. repeat intro. specialize (H i a0). rewrite nth_error_app1 in H. specialize (H H0). destruct H. split; intros. apply H. rewrite nth_error_app1. trivial. apply nth_error_Some; congruence. apply H1. rewrite nth_error_app1. trivial. apply nth_error_Some; congruence. apply nth_error_Some; congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset