A preliminary version of this work (without pairing heaps) is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this publication is available here.
[2015-03-17] Added pairing heaps by Hauke Brinkop.
[2016-07-12] Moved splay heaps from here to Splay_Tree
[2016-07-14] Moved pairing heaps from here to the new Pairing_Heap
Theories of Amortized_Complexity