Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
a ≤ bOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists h. h + a = bThe unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Checked theorems using this definition
CD0004 · finite_bit_subset_pointwise_leCD0005 · finite_bit_count_subset_leCD0006 · finite_add_le_addCD0007 · finite_add_lt_of_lt_of_leCD0008 · finite_add_lt_of_le_of_ltCD0009 · finite_sum_entry_leCD000B · finite_sum_pointwise_strict_atCD002F · finite_modular_sumset_prefix_existsCD0042 · prime_cauchy_davenport_normalized_bounded_induction