fact: Definition ptree_pop (p : ptree) : T * pheap := match p with | PTsome v l => (v, match l with | nil => PHnone | lh :: lt => PHsome (ptree_merge_pairs lh lt) end) end.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)