PA000Q

le_succ_self

Stable checked-use theorem · independently closed

Every natural number is below its successor.

Exact expanded PA statement

forall n. n <= S n

Structural proof guide

Generated structural guide

Every natural number is below its successor.

Use the direct prerequisites zero_add, add_succ_left as previously established PA formulas.

The proof proceeds by certified simplification (1).

Referenced ingredients

PA0001 zero_add PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0001 zero_add PA000E add_succ_left

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA002I bounded_beta_exclusive_recode_invariant 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. 0001intro n
  2. 0002exists 1
  3. 0003simp [add_succ_left, zero_add]