PA0008

zero_or_succ

Stable checked-use theorem · independently closed

Every natural is either zero or the successor of a natural.

Exact expanded PA statement

forall n. n = 0 \/ exists k. n = S k

Structural proof guide

Generated structural guide

Every natural is either zero or the successor of a natural.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA000I bounded_common_multiple_step PA000W le_eq_or_lt PA001C division_remainder_succ PA001D division_remainder_exists PA002E division_remainder_unique PA00AG prime_bounded_square_one_cases

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. 0001induction n
  2. 0002left
  3. 0003refl
  4. 0004right
  5. 0005exists n
  6. 0006refl