BT0002

add_comm

Stable · empty-context checked

Addition is commutative.

Exact expanded PA statement

forall n m. n + m = m + n

Structural proof guide

Addition is commutative.

Direct prerequisites: zero_add, add_succ_left. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT0001 add_succ_left

Direct dependents

BT0005 mul_succ_left BT000V add_left_cancel BT0013 le_add_right BT0015 add_le_add_left BT001N mul_lt_mul_succ_left_nonzero BT001R division_block_upper BT001S positive_quotient_gap_impossible BT001X add_eq_zero_left BT002G factor_difference BT0032 add_permute_outer BT0033 balanced_bezout_euclid_step BT0037 common_divisor_divides_balanced_result BT003Q mod_eq_trans BT003R mod_eq_add BT003W mod_eq_bounded_unique BT003X mod_eq_to_remainder_decomposition BT004C bezout_mod_left BT004E mod_eq_predecessor_cancel BT004O beta_moduli_coprime_of_lt_bounded_common_multiple BT00K5 beta_sum_pointwise_add BT00MY add_shuffle_middle BT00QK power_divides_exponent_antitone BT00R0 ceil_div_six_shift BT00R1 ceil_div_six_total BT00RD mul_le_cancel_left_nonzero BT00RG double_triple_remainder_complement_budget BT00SN pow_exponent_monotone_from_total BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00TL choose_symmetry BT00U0 four_power_central_recurrence_step BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W7 linear_square_budget BT00W8 bertrand_scaled_budget_root_32 BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37 BT00X1 six_block_window_decomposition_above_thirty_two BT00XC add_lt_cancel_left BT00XG division_double_quotient_bit BT00XJ pow_le_pow_of_exponent_le BT00XQ power_quotient_prefix_sum_extend_zero BT00Y2 division_successor_quotient_divisor_le BT00Y3 beta_sum_double_carry_exact BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YB division_first_two_of_two_three_range BT010G floor_sqrt_third_quotient_gap_exists BT010I third_quotient_double_gap_exists BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0112 no_bertrand_high_contribution_interval_eq_one BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one BT011O bertrand_add_swap_nested BT0120 bertrand_cover_eighty_three_one_hundred_sixty_three BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one BT0123 bertrand_cutoff_lt_final_prime

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002induction m
  3. 0003simp [zero_add]
  4. 0004simp [add_succ_left, IH]