Readable signature
Le(a,b)Exact expansion
exists h. h + a = bThis node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
none
Used by definitions
Used by theorem statements or local proof propositions
BT000E le_refl BT000F le_trans BT000J le_antisymm BT000K le_total BT000W zero_le BT000X le_succ_self BT000Y le_zero BT0012 le_add_left BT0013 le_add_right BT0014 add_le_add_right BT0015 add_le_add_left BT0016 succ_le_succ BT0017 le_of_succ_le_succ BT0018 le_succ BT0019 lt_to_le BT001C le_eq_or_lt BT001D lt_of_lt_of_le BT001E lt_of_le_of_lt BT001G le_or_lt BT001I lt_not_le BT001J le_not_lt BT001L mul_le_mul_left BT001M mul_le_mul_right BT002D divisor_le_nonzero BT002U gcd_exists_up_to BT002V gcd_exists_relational BT0034 gcd_balanced_bezout_exists_up_to BT0035 gcd_balanced_bezout_exists BT003D factor_property_succ BT003E factor_search_up_to BT003F prime_or_composite BT003J proper_factor_lt BT003K prime_divisor_exists_up_to BT004O beta_moduli_coprime_of_lt_bounded_common_multiple BT004P beta_moduli_pairwise_coprime_bounded BT0053 beta_value_le_code BT0054 base_le_beta_modulus BT0055 le_scaled_nonzero BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT005B beta_exclusive_recode_invariant_step BT005C bounded_beta_exclusive_recode_invariant BT005D beta_prefix_extend BT005E beta_prefix_product_trace_exists BT005K beta_product_succ_append BT0069 beta_factor_divides_product BT007V beta_repeat_succ_extend BT0085 beta_range_succ_extend BT0089 beta_prefix_sum_trace_exists BT008P bit_count_bounded BT0097 lt_three_cases BT00AA finite_lt_succ_eq_or_lt BT00JD eisenstein_initial_segment_bit_count_functional BT00JE eisenstein_initial_segment_bit_count_exact BT00PS bounded_prime_interval_search BT00PV mul_le_mul BT00PW le_mul_of_one_le_right BT00PX le_mul_of_one_le_left BT00PY pow_base_monotone BT00Q0 one_le_pow BT00Q5 bounded_power_valuation_search BT00Q6 bounded_power_valuation_exists BT00Q8 power_valuation_functional BT00QA power_valuation_dominates BT00QE succ_le_mul_of_two_le_right BT00QF prime_power_exponent_le BT00QG prime_power_divides_exponent_le_value BT00QK power_divides_exponent_antitone BT00QR power_valuation_mul_lower BT00QS power_valuation_mul_upper BT00QT prime_power_valuation_mul BT00R1 ceil_div_six_total BT00R2 ceil_div_six_functional BT00R6 floor_sqrt_lower_bound BT00R9 square_lt_successor_square BT00RC floor_sqrt_monotone BT00RD mul_le_cancel_left_nonzero BT00RF ceil_div_six_le_of_upper BT00RG double_triple_remainder_complement_budget BT00RH canonical_double_triple_remainder_complement_budget BT00RI floor_ceil_complement_budget BT00RJ floor_ceil_division_budget BT00SB prime_power_divides_exponent_le_valuation BT00SC power_divides_of_exponent_le_valuation BT00SN pow_exponent_monotone_from_total BT00SU initial_segment_prefix_sum_exists BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00SY bertrand_hj_six_step_from_total BT00T6 beta_pascal_table_prefix_extend BT00TI choose_succ_succ_of_lt BT00TM choose_positive BT00TY mul_lt_mul_right_nonzero BT00UW primorial_interval_factor_prefix_shift BT00VA factorial_prime_divides_of_le BT00VB factorial_prime_le_of_divides BT00VC choose_prime_divides_between BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle BT00VI primorial_even_interval_le_central BT00VJ primorial_odd_interval_le_middle BT00VK central_binom_strong_upper_step BT00VM central_binom_strong_upper_of_laws BT00VO central_binom_strong_upper BT00VP central_binom_odd_middle_le_four_pow BT00VR double_half_predecessor_data BT00VT central_binom_nonzero_strong_upper BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded BT00VW primorial_le_four_pow BT00VX central_binom_prime_divisor_le_double BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT00W3 pow_block_bound_from_total BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00W7 linear_square_budget BT00W8 bertrand_scaled_budget_root_32 BT00W9 bertrand_scaled_budget_root_33 BT00WA bertrand_scaled_budget_root_34 BT00WB bertrand_scaled_budget_root_35 BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37 BT00WE ceil_div_six_budget_of_scaled_le BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total BT00WL pow_eleven_double_block_le_pow_four_even_from_total BT00WM pow_eleven_double_block_le_pow_four_odd_from_total BT00WN pow_six_ten_block_le_pow_four_thirteen_block_from_total BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00WW bertrand_hj_base_window_thirty_two_from_total BT00X0 floor_sqrt_factorized_threshold_thirty_two BT00X1 six_block_window_decomposition_above_thirty_two BT00X2 bertrand_hj_six_block_iterate_from_total BT00X3 bertrand_hj_envelope_thirty_two BT00X4 bertrand_floor_power_product_le_h_from_total BT00X5 bertrand_four_power_product_le_of_sum_from_total BT00X6 bertrand_main_inequality_factorized_from_total BT00X7 bertrand_main_inequality_factorized BT00X8 bertrand_main_inequality_nat BT00X9 beta_product_pointwise_le BT00XA beta_product_uniform_le_pow BT00XJ pow_le_pow_of_exponent_le BT00XK pow_tail_strict_of_square BT00XO prime_power_quotient_zero_of_exponent_gt BT00XP power_quotient_prefix_tail_entry_zero BT00XQ power_quotient_prefix_sum_extend_zero BT00Y2 division_successor_quotient_divisor_le BT00Y5 central_binom_prime_power_contribution_le_double BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00Y7 central_binom_prime_square_tail_valuation_le_one BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YA prime_square_tail_of_two_three_range BT00YB division_first_two_of_two_three_range BT00YE central_binom_prime_valuation_zero_two_thirds_range BT00YF division_three_scaled_upper_of_quotient_lt BT00YG central_binom_prime_valuation_zero_above_third_quotient BT00YH floor_sqrt_above_root_power_two_strict BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YJ no_bertrand_central_nonzero_valuation_live_ranges BT00YK no_bertrand_central_nonzero_valuation_factor_ranges BT00YL no_bertrand_central_nonzero_contribution_factor_ranges BT00YM no_bertrand_central_prime_contribution_ranges BT0102 prime_contribution_cofactor_prime_contradiction BT0103 prime_contribution_cofactor_eq_one BT0104 prime_contribution_reverse_divides BT0105 prime_contribution_product_eq BT0106 prime_contribution_complete_exists BT0107 central_binom_prime_contribution_product_exists BT0108 no_bertrand_central_contribution_choice_ranges BT010A two_lt_double_lower_six BT010B floor_sqrt_two_le_of_two_lt BT010C three_mul_le_square_of_three_le BT010D floor_sqrt_three_mul_le_double BT010E division_quotient_lower_of_scaled_le BT010F floor_sqrt_le_third_quotient BT010G floor_sqrt_third_quotient_gap_exists BT010H division_quotient_le_dividend BT010I third_quotient_double_gap_exists BT010P prime_contribution_interval_prefix_shift BT010V no_bertrand_small_contribution_choice_le_double BT010W no_bertrand_middle_contribution_choice_le_selector BT010X no_bertrand_high_contribution_choice_eq_one BT010Y no_bertrand_small_contribution_product_le_power BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0112 no_bertrand_high_contribution_interval_eq_one BT0113 central_binom_factorization_small BT0114 central_binom_le_of_no_bertrand_prime BT0115 bertrand_eventually_closed_upper BT0117 factor_pair_has_small_member_below_square BT0118 nonprime_has_small_prime_divisor_below_square BT0119 prime_of_no_small_prime_divisor_below_square BT011A prime_le_twenty_two_cases BT011B nonzero_remainder_not_multiple BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one BT011Q bertrand_covering_interval BT011Y bertrand_cover_forty_three_eighty_three BT0120 bertrand_cover_eighty_three_one_hundred_sixty_three BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one BT0124 bertrand_small_closed_upper BT0125 bertrand_closed_upper BT0127 bertrand_strict