PA002B

add_left_cancel

Stable checked-use theorem · independently closed

A common left addend can be cancelled.

Exact expanded PA statement

forall a b c. a + b = a + c -> b = c

Structural proof guide

Generated structural guide

A common left addend can be cancelled.

Use the direct prerequisites add_comm, add_right_cancel as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000F add_comm PA0012 add_right_cancel

Proof neighborhood

Direct dependencies

PA000F add_comm PA0012 add_right_cancel

Direct dependents

PA002D positive_quotient_gap_impossible PA002E division_remainder_unique PA003T beta_range_injective PA00AG prime_bounded_square_one_cases PA00D1 mod_eq_add_cancel_left

Formal 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.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro h
  5. 0005specialize add_right_cancel b
  6. 0006specialize add_right_cancel c
  7. 0007specialize add_right_cancel a
  8. 0008apply add_right_cancel
  9. 0009trans a + b
  10. 0010apply add_comm
  11. 0011trans a + c
  12. 0012exact h
  13. 0013apply add_comm