(* Title: Sort.thy Author: Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *) section ‹Verification of Heap Sort› theory Heap imports RemoveMax begin subsection ‹Defining tree and properties of heap›