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.
Readable signature
Le(a,b)Exact expansion
exists h. h + a = bThis node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
none
Used by definitions
Used by theorem statements or local proof propositions
PA000Q le_succ_self PA000R le_trans PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA000X lt_to_le PA001A le_refl PA001B le_zero PA001K gcd_balanced_bezout_exists_up_to PA001L gcd_balanced_bezout_exists PA001R beta_moduli_coprime_of_lt_bounded_common_multiple PA001S beta_moduli_pairwise_coprime_bounded PA001U beta_exclusive_accumulated_product_step PA002A le_total PA002G beta_exclusive_recode_congruence_step PA002H beta_exclusive_recode_invariant_step PA002I bounded_beta_exclusive_recode_invariant PA002J le_add_left PA002K succ_le_succ PA002M mul_le_mul_right PA002N le_scaled_nonzero PA002O le_succ PA002P base_le_beta_modulus PA002Q new_value_lt_scaled_base PA002R beta_value_le_code PA002S le_add_right PA002T beta_value_lt_scaled_base PA002X beta_prefix_extend PA002Y beta_range_succ_extend PA0033 lt_of_le_of_lt PA0034 beta_half_range_entry_bounds PA0035 gcd_exists_up_to PA0036 gcd_exists_relational PA0039 divisor_le_nonzero PA003A lt_not_le PA003B le_or_lt PA003D finite_lt_succ_eq_or_lt PA003F zero_le PA003G beta_prefix_sum_trace_exists PA003J add_le_add_right PA003K add_le_add_left PA003W beta_prefix_product_trace_exists PA0044 beta_repeat_succ_extend PA005L quadratic_residue_search_up_to PA005M quadratic_residue_bounded_decidable_nonzero PA0063 prime_bounded_nonzero_mod_inverse PA0069 le_antisymm PA006L lt_of_lt_of_le PA006M mul_le_mul_left PA006Y odd_upper_remainder_reflection PA0070 gauss_pointwise_signed_half_representative PA0071 gauss_pointwise_signed_half_choice PA0072 gauss_half_range_signed_choices PA0073 gauss_signed_half_prefix_extend PA0074 gauss_signed_half_prefix_exists PA0075 gauss_half_range_signed_prefix_exists PA0076 gauss_signed_half_prefix_all_bits PA0077 gauss_signed_half_bit_count_exists PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007D beta_magnitude_predecessor_recode_exists PA007E gauss_signed_half_predecessor_recode_exists PA007P gauss_signed_pointwise_mul_scale_mod PA007R gauss_signed_pointwise_mul_product_mod PA007S beta_magnitude_predecessor_recode_bounded PA007T beta_magnitude_predecessor_recode_reflect PA007U beta_magnitude_predecessor_recode_injective PA007V gauss_predecessor_half_range_aligned PA007Y gauss_magnitude_product_eq_half_range PA0080 gauss_signed_products_balance_mod PA0082 prime_positive_bounded_product_coprime PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA0089 bounded_nonzero_not_divides PA008B prime_mul_index_map_exists_up_to PA008K prime_range_product_coprime PA008S prime_scaled_inverse_prefix_exists_bounded PA009C prime_scaled_inverse_unique PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA00A6 prime_inverse_prefix_exists_bounded PA00AG prime_bounded_square_one_cases PA00B3 beta_magnitude_predecessor_recode_surjective PA00B4 finite_bounded_nonendpoint_injective_coverage PA00BB pair_order_terminal_state_magnitude_range PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BD pair_order_terminal_successor_product_eq_range_two PA00BE prime_wilson_terminal_product_package_exists PA00BV arbitrary_gauss_lemma_complete PA00C3 odd_half_positive_complement_exists PA00C6 odd_signed_division_branch_exact PA00CO odd_signed_division_congruence_mod_two PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00CR gauss_eisenstein_terminal_sums_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00CY beta_magnitude_sum_permutation_exact PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00D8 distinct_odd_prime_half_products_ne PA00D9 distinct_odd_prime_half_cell_oriented PA00DH distinct_odd_prime_half_row_count_choices_bounded PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded PA00DL distinct_odd_prime_half_row_count_prefix_exists PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero PA00DR odd_half_division_quotient_bounded PA00DS nonzero_remainder_division_positive_multiple_threshold PA00DX eisenstein_initial_segment_bit_count_functional PA00DY eisenstein_initial_segment_bit_count_exact PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient