PA0067

drop_add_prefix_from_fixed

Stable checked-use theorem · independently closed

A fixed-point equation remains fixed after dropping an additive prefix.

Exact expanded PA statement

forall a b n. (b + a) + n = n -> a + n = n

Structural proof guide

Generated structural guide

A fixed-point equation remains fixed after dropping an additive prefix.

Use the direct prerequisites zero_add, add_succ_left, no_succ_add_fixed as previously established PA formulas.

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

Referenced ingredients

PA0001 zero_add PA000E add_succ_left PA000Y no_succ_add_fixed

Proof neighborhood

Direct dependencies

PA0001 zero_add PA000E add_succ_left PA000Y no_succ_add_fixed

Direct dependents

PA0068 antisymm_from_witnesses

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. 0002induction b
  3. 0003intro n
  4. 0004intro h
  5. 0005specialize zero_add a
  6. 0006rewrite zero_add at h
  7. 0007exact h
  8. 0008intro n
  9. 0009intro h
  10. 0010exfalso
  11. 0011specialize no_succ_add_fixed (b + a)
  12. 0012specialize no_succ_add_fixed n
  13. 0013apply no_succ_add_fixed
  14. 0014specialize add_succ_left b
  15. 0015specialize add_succ_left a
  16. 0016rewrite add_succ_left at h
  17. 0017exact h