PA0012

add_right_cancel

Stable checked-use theorem · independently closed

A common right addend can be cancelled.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A common right addend can be cancelled.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (1), equality transport (4).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0013 factor_difference PA002B add_left_cancel PA006S mul_left_cancel_nonzero PA006T odd_half_unique PA006Y odd_upper_remainder_reflection

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. 0003induction c
  4. 0004intro h
  5. 0005rewrite PA3 at h
  6. 0006rewrite PA3 at h
  7. 0007exact h
  8. 0008intro h
  9. 0009apply IH
  10. 0010apply PA2
  11. 0011rewrite PA4 at h
  12. 0012rewrite PA4 at h
  13. 0013exact h