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.
Exact expanded PA statement
forall n m. n + m = m + nStructural proof guide
Generated structural guide
Addition is commutative.
Use the direct prerequisites zero_add, add_succ_left as previously established PA formulas.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA000G mul_succ_left PA000J add_eq_zero_left PA0013 factor_difference PA001I add_permute_outer PA001J balanced_bezout_euclid_step PA001O common_divisor_divides_balanced_result PA001R beta_moduli_coprime_of_lt_bounded_common_multiple PA001W bezout_mod_left PA0022 mod_eq_add PA0024 mod_eq_trans PA0025 mod_eq_predecessor_cancel PA002B add_left_cancel PA002D positive_quotient_gap_impossible PA002S le_add_right PA002U mod_eq_bounded_unique PA002V mod_eq_to_remainder_decomposition PA003C remainder_decomposition_to_mod_eq PA003K add_le_add_left PA005D predecessor_square_mod_one PA006I odd_add_odd PA006N division_block_upper PA006Y odd_upper_remainder_reflection PA0070 gauss_pointwise_signed_half_representative PA007B gauss_mixed_sign_scaled_source_impossible PA007C gauss_signed_half_magnitude_injective PA0090 euler_pair_iteration_previous_balance PA0091 euler_pair_iteration_step_short PA00A2 prime_two_or_terminal_odd_shape PA00AG prime_bounded_square_one_cases PA00C3 odd_half_positive_complement_exists PA00C4 predecessor_multiple_mod_complement PA00CI odd_to_mod_two_one PA00CL odd_reflected_remainder_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00CU beta_sum_replace_balance PA00D2 mod_two_cancel_middle PA00DQ odd_half_cross_product_gap PA00DS nonzero_remainder_division_positive_multiple_threshold PA00EP beta_sum_pointwise_addFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
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