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
Lt(a,b)Exact expansion
exists h. h + S 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
PD0007 DivRem PD0014 Product PD0015 Sum PD0016 AllBits PD0018 Range PD0019 Repeat PD0022 BoundedQRes PD0024 BoundedPrefix PD0025 InjectivePrefix PD0026 SurjectivePrefix PD0027 ContainsPrefix PD0028 AllPrime PD0029 Sorted PD0030 UnitResidue PD0032 BoundedNonzeroInverse PD0036 InverseIndex PD0037 InversePrefix PD0038 ScaledInverseIndex PD0039 ScaledInversePrefix PD0040 DivisionPrefixUsed by theorem statements or local proof propositions
PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA000X lt_to_le PA0010 lt_irrefl_expanded PA0011 lt_trichotomy PA001K gcd_balanced_bezout_exists_up_to PA001R beta_moduli_coprime_of_lt_bounded_common_multiple PA001U beta_exclusive_accumulated_product_step PA002C lt_not_eq_add_middle PA002D positive_quotient_gap_impossible PA002E division_remainder_unique PA002G beta_exclusive_recode_congruence_step PA002H beta_exclusive_recode_invariant_step PA002I bounded_beta_exclusive_recode_invariant PA002K succ_le_succ PA002L one_le_of_ne_zero PA002N le_scaled_nonzero PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base PA002U mod_eq_bounded_unique PA002V mod_eq_to_remainder_decomposition PA002W beta_at_of_mod_eq_bound PA002X beta_prefix_extend PA002Y beta_range_succ_extend PA0032 beta_range_entry_eq PA0033 lt_of_le_of_lt PA0034 beta_half_range_entry_bounds PA0035 gcd_exists_up_to PA0039 divisor_le_nonzero PA003A lt_not_le PA003B le_or_lt PA003D finite_lt_succ_eq_or_lt PA003E beta_at_self_of_bound PA003G beta_prefix_sum_trace_exists PA003H beta_sum_exists PA003T beta_range_injective PA003U ne_zero_of_one_le PA003W beta_prefix_product_trace_exists PA003X beta_product_exists PA0044 beta_repeat_succ_extend PA004C beta_repeat_entry_eq PA004H finite_contains_decidable PA004I finite_bounded_last_succ PA004J beta_prefix_replace_exists PA004K beta_prefix_swap_last_from_entries PA004L finite_bounded_entry_lt PA004M finite_swap_last_bounded PA004N beta_prefix_swap_last_reflect PA004O finite_swap_last_injective PA004P finite_bounded_prefix_without_top PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro PA004U finite_swap_last_surjective_back PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective PA004X finite_fixed_last_prefix_bounded PA004Y beta_product_transport_prefix PA0051 beta_product_functional PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA0054 beta_reindex_alignment_swap_last PA005F beta_repeat_transport_entry PA005G pow_functional PA005J mod_eq_decidable_from_remainders PA005L quadratic_residue_search_up_to PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA006A beta_range_transport_entry PA006B factorial_functional PA006K beta_sum_trace_functional PA006L lt_of_lt_of_le PA006N division_block_upper PA006O lt_trans 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 PA0079 prime_scaled_same_target_unique PA007A gauss_same_sign_scaled_source_unique PA007B gauss_mixed_sign_scaled_source_impossible PA007C gauss_signed_half_magnitude_injective PA007D beta_magnitude_predecessor_recode_exists PA007E gauss_signed_half_predecessor_recode_exists PA007F beta_sign_factor_prefix_extend PA007G beta_sign_factor_prefix_exists PA007H beta_sign_factor_prefix_drop_last PA007I beta_sign_factor_product_power PA007J beta_sign_factor_product_power_exists PA007K beta_pointwise_mul_prefix_extend PA007L beta_pointwise_mul_prefix_exists PA007M beta_pointwise_mul_prefix_drop_last PA007N beta_product_pointwise_mul_exact PA007O beta_pointwise_mul_product_exists PA007P gauss_signed_pointwise_mul_scale_mod PA007Q beta_product_pointwise_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 PA007W beta_product_reindex_fixed_last PA007X beta_product_permutation_invariant PA007Y gauss_magnitude_product_eq_half_range PA0080 gauss_signed_products_balance_mod PA0081 beta_product_pointwise_coprime PA0082 prime_positive_bounded_product_coprime PA0083 prime_half_range_product_coprime PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA0086 nondivisor_canonical_remainder_exists PA0089 bounded_nonzero_not_divides PA008A mod_eq_zero_to_dvd_nonzero PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008D fermat_index_map_bounded PA008E prime_mul_index_map_injective PA008F beta_range_one_entry_eq_succ PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod PA008I prime_mul_residue_reindex_exists PA008J prime_mul_residue_product_balance PA008K prime_range_product_coprime PA008P prime_scaled_inverse_target_nonzero PA008Q prime_scaled_inverse_exists PA008R prime_scaled_inverse_prefix_extend PA008S prime_scaled_inverse_prefix_exists_bounded PA008T prime_scaled_inverse_prefix_exists PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008X scaled_pair_order_state_zero PA008Y adjacent_scaled_orbit_history_zero PA0092 finite_covers_into_or_omits PA0093 finite_inverse_choice_prefix_extend PA0094 finite_inverse_choice_prefix_exists PA0095 finite_inverse_choice_bounded_into PA0096 finite_inverse_choice_injective PA0097 finite_short_cover_impossible PA0098 finite_short_prefix_omits PA0099 scaled_inverse_prefix_entry_sound PA009A scaled_inverse_prefix_mate_predecessor PA009D scaled_inverse_prefix_extensional PA009E scaled_inverse_prefix_involutive PA009H scaled_inverse_prefix_no_fixed_of_not_qres PA009I scaled_inverse_prefix_choose_omitted_orbit PA009J scaled_orbit_closed_unused_mate PA009K beta_prefix_append_two_exists PA009L beta_prefix_append_two_reflect PA009M beta_prefix_append_two_scaled_orbit_closed PA009N beta_prefix_append_two_injective PA009O scaled_inverse_pair_order_choose_append PA009P beta_prefix_append_two_bounded_into PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA009S adjacent_scaled_orbit_history_append PA009T scaled_inverse_pair_order_paired_state_step PA009V scaled_inverse_pair_order_paired_iteration PA009W scaled_inverse_pair_order_terminal_package PA009X scaled_pair_order_successor_lift_adjacent_targets PA00A0 beta_adjacent_target_pairs_product_power PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00A4 prime_inverse_index_exists PA00A5 prime_inverse_prefix_extend PA00A8 orbit_closed_prefix_zero PA00A9 nonendpoint_prefix_zero PA00AA pair_order_state_zero PA00AB paired_inverse_witness_zero PA00AE finite_prefix_choose_unused_nonendpoint PA00AF inverse_prefix_entry_sound PA00AG prime_bounded_square_one_cases PA00AH prime_inverse_prefix_fixed_cases PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AL bounded_inverse_index_unique PA00AM inverse_prefix_extensional PA00AN inverse_prefix_involutive PA00AO inverse_prefix_zero_fixed PA00AP inverse_prefix_last_fixed PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AR prime_choose_unused_nonendpoint_orbit PA00AS orbit_closed_unused_mate PA00AT beta_prefix_append_two_orbit_closed PA00AU beta_prefix_append_two_nonendpoint PA00AV prime_pair_order_choose_append PA00AW prime_pair_order_choose_append_injective PA00AX prime_pair_order_choose_append_state PA00AY paired_inverse_witness_append PA00B0 prime_pair_order_paired_state_step PA00B1 prime_pair_order_paired_iteration PA00B2 prime_pair_order_paired_terminal_state_exists PA00B3 beta_magnitude_predecessor_recode_surjective PA00B4 finite_bounded_nonendpoint_injective_coverage PA00B5 pair_order_state_terminal_coverage PA00B6 pair_order_successor_lift_exists PA00B7 paired_successor_lift_adjacent_units PA00B8 paired_pair_order_factor_code_exists PA00B9 beta_adjacent_unit_pairs_product_one PA00BA paired_pair_order_product_one_exists 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 PA00BF prime_terminal_range_two_product_mod_one_exists PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor PA00BM quadratic_nonresidue_half_power_mod_predecessor PA00BN bounded_euler_criterion_dichotomy PA00BP odd_prime_one_not_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BV arbitrary_gauss_lemma_complete PA00BW beta_scaled_successor_prefix_from_pointwise PA00BX beta_division_prefix_extend PA00C0 prime_scaled_half_division_prefix_exists PA00C1 prime_scaled_half_quotient_sum_exists PA00C2 odd_half_strictly_below_modulus PA00C3 odd_half_positive_complement_exists PA00C5 canonical_remainder_from_mod PA00C6 odd_signed_division_branch_exact PA00CO odd_signed_division_congruence_mod_two PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00CR gauss_eisenstein_terminal_sums_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00CT beta_sum_transport_prefix PA00CU beta_sum_replace_balance PA00CV beta_sum_swap_last_invariant PA00CW beta_sum_reindex_fixed_last PA00CX beta_sum_permutation_invariant 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 PA00DA distinct_odd_prime_half_cell_indicator_choice PA00DB distinct_odd_prime_half_row_indicator_choices PA00DC eisenstein_row_indicator_prefix_extend PA00DD eisenstein_row_indicator_prefix_exists PA00DE eisenstein_row_indicator_prefix_all_bits PA00DF distinct_odd_prime_half_row_count_exists PA00DG distinct_odd_prime_half_row_count_choice PA00DH distinct_odd_prime_half_row_count_choices_bounded PA00DI eisenstein_rectangle_row_count_prefix_extend PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded PA00DL distinct_odd_prime_half_row_count_prefix_exists PA00DM distinct_odd_prime_half_rectangle_total_exists PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero PA00DO distinct_primes_bounded_scaled_remainder_nonzero PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero PA00DQ odd_half_cross_product_gap PA00DR odd_half_division_quotient_bounded PA00DS nonzero_remainder_division_positive_multiple_threshold PA00DT eisenstein_row_indicator_prefix_to_initial_segment PA00DU eisenstein_initial_segment_prefix_all_bits PA00DV eisenstein_initial_segment_decoded_choice PA00DX eisenstein_initial_segment_bit_count_functional PA00DY eisenstein_initial_segment_bit_count_exact PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient PA00E2 distinct_odd_prime_semantic_row_equals_decoded_quotient PA00E3 distinct_odd_prime_quotient_entry_matches_rectangle PA00E4 distinct_odd_prime_quotient_sum_transports_to_rectangle PA00E5 distinct_odd_prime_quotient_sum_equals_rectangle_total PA00E6 eisenstein_rectangle_decoded_row_count PA00E7 eisenstein_transposed_outer_column_choices PA00E8 eisenstein_transposed_column_prefix_extend PA00E9 eisenstein_transposed_column_prefix_exists PA00EA eisenstein_row_indicator_decoded_choice PA00EB eisenstein_transposed_column_prefix_all_bits PA00EC eisenstein_transposed_decoded_cell_bits_complementary PA00ED eisenstein_transposed_column_pointwise_complement PA00EE complementary_bit_counts_add_length PA00EF eisenstein_row_transposed_column_count_partition PA00EG eisenstein_transposed_column_count_choices PA00EH eisenstein_transposed_column_count_prefix_extend PA00EI eisenstein_transposed_column_count_prefix_exists PA00EJ eisenstein_transposed_column_count_total_exists PA00EM eisenstein_transposed_column_count_decoded_witness PA00EN eisenstein_transposed_column_count_decoded_partition PA00EO eisenstein_transposed_column_count_matches_decoded_constant PA00EP beta_sum_pointwise_add PA00EQ eisenstein_rectangle_plus_column_count_total PA00ER eisenstein_transposed_column_count_prefix_forget PA00ES eisenstein_zero_width_rectangle_sum_zero PA00ET eisenstein_row_indicator_prefix_succ_restrict PA00EU eisenstein_successor_row_count_decompose PA00EV eisenstein_successor_row_split_choices PA00EW eisenstein_successor_row_split_prefix_extend PA00EX eisenstein_successor_row_split_prefix_exists PA00EY eisenstein_successor_rectangle_row_split_prefix_exists PA00F0 eisenstein_successor_row_split_reduced_rectangle_prefix PA00F1 eisenstein_successor_row_split_decoded_add PA00F2 eisenstein_successor_row_split_sum_add PA00F3 eisenstein_fubini_column_count_prefix_succ_restrict PA00F4 eisenstein_transposed_column_decoded_choice PA00F5 eisenstein_cell_indicator_choice_unique PA00F6 eisenstein_transposed_column_counts_extensional PA00F7 eisenstein_fubini_column_count_witness_retarget PA00F8 eisenstein_fubini_column_count_prefix_retarget_predecessor PA00F9 eisenstein_successor_terminal_bit_matches_last_column PA00FA eisenstein_successor_terminal_prefix_to_last_column PA00FB eisenstein_successor_terminal_sum_matches_last_column PA00FC eisenstein_fubini_universal PA00FD eisenstein_constructed_column_total_equals_swapped_total PA00FE eisenstein_rectangle_floor_sum_identity PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity PA00FG distinct_odd_primes_gauss_eisenstein_data_exists