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. Le(n,n)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
1 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n. n <= nProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
BT002V gcd_exists_relational BT0035 gcd_balanced_bezout_exists BT003E factor_search_up_to BT003L prime_divisor_exists BT005A beta_exclusive_recode_congruence_step BT005D beta_prefix_extend BT005E beta_prefix_product_trace_exists BT005G beta_product_functional BT005J beta_product_succ_decompose BT005K beta_product_succ_append BT0083 pow_successor_decompose BT0089 beta_prefix_sum_trace_exists BT008B beta_sum_trace_functional BT008F beta_sum_succ_decompose BT008K all_bits_last_succ BT0092 factorial_succ_decompose BT00DH beta_product_pointwise_coprime BT00JC beta_all_one_bit_count_exact BT00JD eisenstein_initial_segment_bit_count_functional BT00K5 beta_sum_pointwise_add BT00PR prime_strictly_above_decidable BT00PS bounded_prime_interval_search BT00PY pow_base_monotone BT00Q0 one_le_pow BT00Q5 bounded_power_valuation_search BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00T6 beta_pascal_table_prefix_extend BT00TC choose_functional BT00TE choose_zero BT00TF beta_pascal_table_diagonal_boundary BT00TG choose_self BT00TI choose_succ_succ_of_lt BT00TJ choose_succ_succ BT00UD primorial_succ_decompose BT00UQ beta_product_prefix_suffix_split BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00VH primorial_odd_interval_divides_middle BT00VM central_binom_strong_upper_of_laws BT00VV primorial_le_four_pow_bounded BT00VW primorial_le_four_pow BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_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 BT00X9 beta_product_pointwise_le BT00XX double_quotient_carry_prefix_exists BT00Y1 bit_count_positive_last_one BT00Y3 beta_sum_double_carry_exact BT010B floor_sqrt_two_le_of_two_lt BT010U beta_product_all_one_exact BT010W no_bertrand_middle_contribution_choice_le_selectorDefinition-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–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n
02Construct an explicit witnessL2–2
Supply the displayed value, then prove that it has the required property.
- L2
exists 0
03Calculate and transport equalitiesL3–3
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L3
simp [zero_add]