BT001B

lt_irrefl_expanded

Stable · empty-context checked

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

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

Direct prerequisites: add_succ_left, no_succ_add_fixed. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT0001 add_succ_left BT000G no_succ_add_fixed

Direct dependents

BT0059 beta_exclusive_accumulated_product_step BT00R2 ceil_div_six_functional BT00RF ceil_div_six_le_of_upper BT00TG choose_self BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00YC double_quotient_carry_prefix_entries_zero BT010B floor_sqrt_two_le_of_two_lt

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. 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