BT000G

no_succ_add_fixed

Stable · empty-context checked

Adding a positive successor cannot leave a natural number fixed.

Exact expanded PA statement

forall p n. S p + n = n -> false

Structural proof guide

Adding a positive successor cannot leave a natural number fixed.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT000H drop_add_prefix_from_fixed BT001B lt_irrefl_expanded

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002induction n
  3. 0003intro h
  4. 0004apply PA1
  5. 0005rewrite PA3 at h
  6. 0006exact h
  7. 0007intro h
  8. 0008apply IH
  9. 0009apply PA2
  10. 0010rewrite PA4 at h
  11. 0011exact h