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.
Statement with defined notation
∀ n. ∀ m. ∀ k. Le(n,m) → Le(m,k) → Le(n,k)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n m k. n <= m -> m <= k -> n <= kProof neighborhood
Direct theorem prerequisites
Direct theorem 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_intervalDefinition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–7
03Construct an explicit witnessL8–8
Supply the displayed value, then prove that it has the required property.
- L8
exists x1 + x
04Calculate and transport equalitiesL9–9
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L9
simp [add_assoc, h_nm_witness, h_mk_witness]