BT000U

add_right_cancel

Stable · empty-context checked

A common right addend can be cancelled.

Exact expanded PA statement

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

Structural proof guide

A common right addend can be cancelled.

Direct prerequisites: none. The authored body proceeds by structural induction (1), equality transport (4).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT000V add_left_cancel BT0022 mul_left_cancel_nonzero BT002G factor_difference

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