proposition: Theorem ptree_pop_correct : forall p, match ptree_pop p with | (v, q) => permut (v :: pheap_to_list q) (ptree_to_list p) end.
proof: Proof. intros [v [|l]]. apply permut_refl. simpl. apply permut_cons. apply ptree_merge_pairs_correct. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)