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
S a ≤ bOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists h. h + S 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
PC0004 · prime_bit_prefix_entryPC0005 · prime_bit_prefix_extendPC0007 · prime_bit_prefix_all_bitsPC000A · beta_sum_entry_lePC000B · prime_count_positive_above_onePC000C · beta_product_bit_weighted_upper_powerPC000D · beta_product_bit_weighted_lower_powerPC000E · beta_cutoff_choice_existsPC0011 · beta_cutoff_prefix_entryPC0012 · beta_cutoff_prefix_extendPC0013 · beta_cutoff_prefix_existsPC0014 · beta_cutoff_count_comparisonPC0015 · binary_power_two_dominates_successorPC0016 · binary_power_two_order_reflects_exponentPC0017 · binary_power_two_strict_order_reflects_exponentPC0019 · central_binom_dominates_pow_twoPC001A · primorial_prefix_decoded_choicePC001B · primorial_factor_choice_one_lePC001C · prime_contribution_prefix_decoded_choicePC001D · central_binom_prime_mask_weighted_upperPC001E · primorial_cutoff_weighted_lowerPC001F · central_binom_prime_count_power_boundPC0021 · binary_split_half_lower_boundPC0023 · double_successor_le_triple_above_onePC0024 · binary_length_positivePC0025 · binary_length_nonzero_componentsPC0026 · binary_half_scale_boundsPC002A · prime_count_chebyshev_upperPC002C · double_successor_le_triple_of_positivePC002D · binary_split_eight_boundPC002E · central_binom_prime_count_exponent_boundPC002F · prime_count_chebyshev_lower_largePC0030 · prime_count_chebyshev_lowerPC0031 · prime_count_chebyshev_boundsPC0033 · prime_bit_prefix_equal_entry