BT011O

bertrand_add_swap_nested

Alpha body-checked · checked-use disabled

Swap the first two addends under a fixed trailing addend.

Exact expanded PA statement

forall a b c. a + (b + c) = b + (a + c)

Structural proof guide

Swap the first two addends under a fixed trailing addend.

Direct prerequisites: add_assoc, add_comm. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm

Direct dependents

BT011P bertrand_add_six_permute BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen 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 a
  2. 0002intro b
  3. 0003intro c
  4. 0004trans (a + b) + c
  5. 0005symm
  6. 0006apply add_assoc
  7. 0007trans (b + a) + c
  8. 0008congr
  9. 0009apply add_comm
  10. 0010refl
  11. 0011apply add_assoc