PA000Y

no_succ_add_fixed

Stable checked-use theorem · independently closed

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

Generated structural guide

Adding a positive successor cannot leave a natural number fixed.

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 (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0010 lt_irrefl_expanded PA0067 drop_add_prefix_from_fixed

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