PA0010

lt_irrefl_expanded

Stable checked-use theorem · independently closed

No natural is strictly below itself, with strict order fully expanded.

Exact expanded PA statement

forall n. ~(exists k. k + S n = n)

Structural proof guide

Generated structural guide

No natural is strictly below itself, with strict order fully expanded.

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

The proof proceeds by case analysis (1).

Referenced ingredients

PA000E add_succ_left PA000Y no_succ_add_fixed

Proof neighborhood

Direct dependencies

PA000E add_succ_left PA000Y no_succ_add_fixed

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA004K beta_prefix_swap_last_from_entries PA004R finite_last_is_top_from_prefix_surjective PA004W finite_bounded_injective_surjective PA004X finite_fixed_last_prefix_bounded PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA0097 finite_short_cover_impossible PA00C3 odd_half_positive_complement_exists PA00CU beta_sum_replace_balance PA00CV beta_sum_swap_last_invariant

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. 0002intro h
  3. 0003cases h
  4. 0004specialize no_succ_add_fixed x
  5. 0005specialize no_succ_add_fixed n
  6. 0006apply no_succ_add_fixed
  7. 0007trans x + S n
  8. 0008trans S (x + n)
  9. 0009apply add_succ_left
  10. 0010symm
  11. 0011apply PA4
  12. 0012exact h_witness