proposition: Theorem pheap_insert_correct : forall p v, permut (ptree_to_list (pheap_insert p v)) (v :: pheap_to_list p).
proof: Proof. intros [|p] v. apply permut_refl. apply ptree_insert_correct. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)