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	31	characters	75964	nodes	61055
propositions	theorems	2	lemmas	182	total	184
concepts	declared	41	defined	25	total	66

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.