Readable signature
Lt(a,b)Exact expansion
exists h. h + S 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
PD0007 DivRem PD0014 Product PD0015 Sum PD0016 AllBits PD0018 Range PD0019 Repeat PD0041 Choose PD0051 FloorSqrt PD0052 CeilDivSixUsed by theorem statements or local proof propositions
BT0010 one_le_of_ne_zero BT0011 ne_zero_of_one_le BT0016 succ_le_succ BT0017 le_of_succ_le_succ BT0019 lt_to_le BT001B lt_irrefl_expanded BT001C le_eq_or_lt BT001D lt_of_lt_of_le BT001E lt_of_le_of_lt BT001F lt_trans BT001G le_or_lt BT001H lt_trichotomy BT001I lt_not_le BT001J le_not_lt BT001K lt_not_eq_add_middle BT001N mul_lt_mul_succ_left_nonzero BT001R division_block_upper BT001S positive_quotient_gap_impossible BT001U division_remainder_unique BT001W multiple_has_zero_remainder BT002D divisor_le_nonzero BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to BT003B multiple_decidable_nonzero BT003D factor_property_succ BT003J proper_factor_lt BT003K prime_divisor_exists_up_to BT003W mod_eq_bounded_unique BT003X mod_eq_to_remainder_decomposition BT0040 beta_at_self_of_bound BT0045 beta_at_of_mod_eq_bound BT004O beta_moduli_coprime_of_lt_bounded_common_multiple 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 BT005F beta_product_exists BT005G beta_product_functional BT005K beta_product_succ_append BT005L beta_product_transport_prefix BT0069 beta_factor_divides_product BT007V beta_repeat_succ_extend BT007X beta_repeat_entry_eq BT007Y beta_repeat_transport_entry BT0082 pow_functional BT0085 beta_range_succ_extend BT0087 beta_range_entry_eq BT0088 beta_range_transport_entry BT0089 beta_prefix_sum_trace_exists BT008A beta_sum_exists BT008B beta_sum_trace_functional BT0090 factorial_functional BT0097 lt_three_cases BT00AA finite_lt_succ_eq_or_lt BT00DH beta_product_pointwise_coprime BT00I9 beta_sum_transport_prefix BT00JA eisenstein_initial_segment_prefix_all_bits BT00JB eisenstein_initial_segment_decoded_choice BT00JD eisenstein_initial_segment_bit_count_functional BT00JE eisenstein_initial_segment_bit_count_exact BT00K5 beta_sum_pointwise_add BT00PR prime_strictly_above_decidable BT00PS bounded_prime_interval_search BT00PW le_mul_of_one_le_right BT00PX le_mul_of_one_le_left BT00Q0 one_le_pow BT00Q1 pow_nonzero_of_one_le BT00Q5 bounded_power_valuation_search BT00QD prime_two_le BT00QE succ_le_mul_of_two_le_right BT00QF prime_power_exponent_le BT00QH power_valuation_successor_not_divides BT00QN prime_power_successor_cancel_cofactor BT00QS power_valuation_mul_upper BT00R2 ceil_div_six_functional BT00R7 floor_sqrt_strict_upper_bound BT00R9 square_lt_successor_square BT00RA floor_sqrt_total BT00RC floor_sqrt_monotone BT00RF ceil_div_six_le_of_upper BT00RG double_triple_remainder_complement_budget BT00RH canonical_double_triple_remainder_complement_budget BT00RJ floor_ceil_division_budget BT00S0 prime_power_quotient_prefix_exists BT00S1 power_quotient_prefix_transport BT00S3 legendre_sum_functional BT00SD eisenstein_initial_segment_indicator_choice BT00SE eisenstein_initial_segment_prefix_extend BT00SF eisenstein_initial_segment_prefix_exists BT00SG division_remainder_successor_cases BT00SH division_successor_quotient_by_bit BT00SI valuation_threshold_bit_decides_power_divides BT00SJ power_quotient_prefix_decoded_divrem BT00SK power_quotient_successor_pointwise_add BT00SN pow_exponent_monotone_from_total BT00SU initial_segment_prefix_sum_exists BT00SV prime_legendre_sum_succ BT00SW bertrand_h_six_step_transport_from_total BT00SY bertrand_hj_six_step_from_total BT00T2 beta_pascal_zero_row_extend BT00T3 beta_pascal_zero_row_exists BT00T4 beta_pascal_row_step_extend BT00T5 beta_pascal_row_step_exists BT00T6 beta_pascal_table_prefix_extend BT00T7 beta_pascal_table_prefix_exists BT00T8 choose_exists BT00T9 beta_pascal_zero_row_pointwise_functional BT00TA beta_pascal_row_step_pointwise_functional BT00TB beta_pascal_table_row_pointwise_functional BT00TC choose_functional BT00TD choose_out_of_range_zero BT00TE choose_zero BT00TF beta_pascal_table_diagonal_boundary BT00TG choose_self BT00TH beta_pascal_table_successor_cell_recurrence BT00TI choose_succ_succ_of_lt BT00TJ choose_succ_succ BT00TY mul_lt_mul_right_nonzero BT00U0 four_power_central_recurrence_step BT00U3 four_pow_central_seed_package BT00U4 four_pow_lt_mul_central_binom BT00U7 primorial_factor_prefix_extend BT00U8 primorial_factor_prefix_exists BT00UA primorial_exists BT00UQ beta_product_prefix_suffix_split BT00UR primorial_interval_factor_prefix_extend BT00US primorial_interval_factor_prefix_exists BT00UW primorial_interval_factor_prefix_shift BT00UX primorial_factor_prefix_restrict_add BT00UY primorial_prefix_interval_split BT00VC choose_prime_divides_between BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00VE primorial_interval_pairwise_coprime BT00VF primorial_interval_divides_choose_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 BT00VS odd_positive_prefix_predecessor_bound BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded BT00VY no_bertrand_central_prime_divisor_le BT00W0 power_valuation_nonzero_exponent_divides_base BT00W2 no_bertrand_central_prime_divisor_ranges 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 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 BT00X9 beta_product_pointwise_le BT00XA beta_product_uniform_le_pow BT00XB add_lt_add BT00XC add_lt_cancel_left BT00XF division_zero_quotient_of_lt BT00XG division_double_quotient_bit 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 BT00XV double_quotient_carry_choice BT00XW double_quotient_carry_prefix_extend BT00XX double_quotient_carry_prefix_exists BT00XY double_quotient_carry_prefix_all_bits BT00Y0 double_quotient_carry_prefix_restrict BT00Y1 bit_count_positive_last_one BT00Y3 beta_sum_double_carry_exact BT00Y4 central_binom_carry_bit_count 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 BT00YC double_quotient_carry_prefix_entries_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients 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 BT00YP prime_contribution_prefix_extend BT00YQ prime_contribution_prefix_exists BT00YS prime_contribution_product_exists BT00YW prime_contribution_prefix_pairwise_coprime BT00YY prime_contribution_product_divides BT0100 prime_contribution_selected_entry 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 BT010J floor_third_double_gap_package BT010K prime_contribution_interval_prefix_extend BT010L prime_contribution_interval_prefix_exists BT010P prime_contribution_interval_prefix_shift BT010Q prime_contribution_prefix_restrict_add BT010R prime_contribution_prefix_interval_split BT010S prime_contribution_product_length_eq_transport BT010U beta_product_all_one_exact 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 BT011R bertrand_cover_one_two BT011S bertrand_cover_two_three BT011T bertrand_cover_three_five BT011U bertrand_cover_five_seven BT011V bertrand_cover_seven_thirteen BT011W bertrand_cover_thirteen_twenty_three BT011X bertrand_cover_twenty_three_forty_three BT0123 bertrand_cutoff_lt_final_prime BT0124 bertrand_small_closed_upper BT0125 bertrand_closed_upper BT0126 bertrand_upper_endpoint_factorization BT0127 bertrand_strict