PA0069

le_antisymm

Stable checked-use theorem · independently closed

The witness-defined order is antisymmetric.

Exact expanded PA statement

forall n m. n <= m -> m <= n -> n = m

Structural proof guide

Generated structural guide

The witness-defined order is antisymmetric.

Use the direct prerequisites antisymm_from_witnesses as previously established PA formulas.

The proof proceeds by case analysis (2).

Referenced ingredients

PA0068 antisymm_from_witnesses

Proof neighborhood

Direct dependencies

PA0068 antisymm_from_witnesses

Direct dependents

PA00AG prime_bounded_square_one_cases

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 m
  3. 0003intro h_nm
  4. 0004intro h_mn
  5. 0005cases h_nm
  6. 0006cases h_mn
  7. 0007apply antisymm_from_witnesses
  8. 0008exact h_nm_witness
  9. 0009exact h_mn_witness