BT000H

drop_add_prefix_from_fixed

Stable · empty-context checked

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

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

Direct prerequisites: zero_add, add_succ_left, no_succ_add_fixed. The authored body proceeds by structural induction (1), equality transport (2).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT0001 add_succ_left BT000G no_succ_add_fixed

Direct dependents

BT000I antisymm_from_witnesses

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