Exact expanded PA statement
forall n m k. n <= m -> m <= k -> n <= kStructural proof guide
Order witnesses compose by addition, so the defined order is transitive.
Direct prerequisites: add_assoc. The authored body proceeds by case analysis (2).
Proof neighborhood
Direct dependencies
Direct dependents
BT001D lt_of_lt_of_le BT004O beta_moduli_coprime_of_lt_bounded_common_multiple BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base BT0059 beta_exclusive_accumulated_product_step BT005C bounded_beta_exclusive_recode_invariant BT00PV mul_le_mul BT00Q0 one_le_pow BT00QE succ_le_mul_of_two_le_right BT00QF prime_power_exponent_le BT00QG prime_power_divides_exponent_le_value BT00RC floor_sqrt_monotone BT00RG double_triple_remainder_complement_budget BT00RI floor_ceil_complement_budget BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00VK central_binom_strong_upper_step BT00VV primorial_le_four_pow_bounded BT00WE ceil_div_six_budget_of_scaled_le BT00WM pow_eleven_double_block_le_pow_four_odd_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 BT00X2 bertrand_hj_six_block_iterate_from_total BT00X4 bertrand_floor_power_product_le_h_from_total BT00X6 bertrand_main_inequality_factorized_from_total BT00Y5 central_binom_prime_power_contribution_le_double BT00YA prime_square_tail_of_two_three_range BT00YB division_first_two_of_two_three_range BT00YH floor_sqrt_above_root_power_two_strict BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YL no_bertrand_central_nonzero_contribution_factor_ranges BT010A two_lt_double_lower_six BT010B floor_sqrt_two_le_of_two_lt BT010D floor_sqrt_three_mul_le_double BT010H division_quotient_le_dividend BT010V no_bertrand_small_contribution_choice_le_double BT010X no_bertrand_high_contribution_choice_eq_one BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0115 bertrand_eventually_closed_upper BT0117 factor_pair_has_small_member_below_square BT0118 nonprime_has_small_prime_divisor_below_square 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_intervalFormal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.