BT000X

le_succ_self

Stable · empty-context checked

Every natural number is below its successor.

Exact expanded PA statement

forall n. n <= S n

Structural proof guide

Every natural number is below its successor.

Direct prerequisites: zero_add, add_succ_left. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0000 zero_add BT0001 add_succ_left

Direct dependents

BT0059 beta_exclusive_accumulated_product_step BT005C bounded_beta_exclusive_recode_invariant BT00R9 square_lt_successor_square

Formal native tactic body

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

  1. 0001intro n
  2. 0002exists 1
  3. 0003simp [add_succ_left, zero_add]