BT000R

nonzero_is_succ

Stable · empty-context checked

Every nonzero natural has a predecessor.

Exact expanded PA statement

forall n. ~(n = 0) -> exists k. n = S k

Structural proof guide

Every nonzero natural has a predecessor.

Direct prerequisites: none. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT004F binary_crt BT00AW prime_is_succ_succ BT0124 bertrand_small_closed_upper

Formal native tactic body

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

  1. 0001induction n
  2. 0002intro h
  3. 0003exfalso
  4. 0004apply h
  5. 0005refl
  6. 0006intro h
  7. 0007exists n
  8. 0008refl