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
DivRem(n,d,q,r)Exact expansion
n = d * q + r /\ exists h. h + S r = dThis 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
Used by definitions
Used by theorem statements or local proof propositions
BT001O division_remainder_succ BT001P division_remainder_exists BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to BT003B multiple_decidable_nonzero BT003X mod_eq_to_remainder_decomposition BT0041 beta_at_exists BT00R1 ceil_div_six_total BT00RH canonical_double_triple_remainder_complement_budget BT00RJ floor_ceil_division_budget BT00S0 prime_power_quotient_prefix_exists BT00S1 power_quotient_prefix_transport BT00SA prime_power_quotient_tail_zero BT00SG division_remainder_successor_cases BT00SH division_successor_quotient_by_bit BT00SJ power_quotient_prefix_decoded_divrem BT00SK power_quotient_successor_pointwise_add BT00SS prime_power_quotient_prefix_last_zero BT00X1 six_block_window_decomposition_above_thirty_two BT00X6 bertrand_main_inequality_factorized_from_total BT00X7 bertrand_main_inequality_factorized BT00X8 bertrand_main_inequality_nat BT00XF division_zero_quotient_of_lt BT00XG division_double_quotient_bit BT00XO prime_power_quotient_zero_of_exponent_gt BT00XP power_quotient_prefix_tail_entry_zero BT00XV double_quotient_carry_choice BT00Y2 division_successor_quotient_divisor_le BT00Y5 central_binom_prime_power_contribution_le_double BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds 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 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 BT0108 no_bertrand_central_contribution_choice_ranges 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 BT010J floor_third_double_gap_package 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