BT001J

le_not_lt

Stable · empty-context checked

A weak inequality excludes strict inequality in the reverse direction.

Exact expanded PA statement

forall a b. (exists k. k + a = b) -> ~ (exists k. k + S b = a)

Structural proof guide

A weak inequality excludes strict inequality in the reverse direction.

Direct prerequisites: lt_not_le. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT001I lt_not_le

Direct dependents

BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro hab
  4. 0004intro hba
  5. 0005specialize lt_not_le b
  6. 0006specialize lt_not_le a
  7. 0007apply lt_not_le
  8. 0008exact hba
  9. 0009exact hab