BT001J

le_not_lt

Stable checked-use theorem · independently kernel verified

A weak inequality excludes strict inequality in the reverse direction.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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 the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

9 script commands · 2 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
lt not le
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hab
  4. L4
    intro hba
02Use earlier factsL5–9

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L5
    specialize lt_not_le b
  2. L6
    specialize lt_not_le a
  3. L7
    apply lt_not_le
  4. L8
    exact hba
  5. L9
    exact hab

Library-wide reading audit

Original exact command ledger · 9 lines
  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