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.