Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" [F. Guidi: "Procedural Representation of CIC Proof Terms" Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].

category	objects
sizes	files	30	characters	46649	nodes	62380
propositions	theorems	2	lemmas	187	total	189
concepts	declared	40	defined	25	total	65

The source files are grouped in planes according to the following table. Notation files covering the whole specification are provided. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).

plane	files
natural numbers with infinity	ynat ( ∞ )	ynat_pred ( ⫰? )	ynat_succ ( ⫯? )	ynat_le ( ?≤? )	ynat_lt ( ?<? )	ynat_minus ( ? - ? )	ynat_plus ( ? + ? )	ynat_max	ynat_min
extensions to the library	arith.ma ( ?^? )
generated logical decomposables	xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )	xoa_props ( ⊥ ) ( ⊤ )

The source files are grouped in directories, one for each plane.