BT000J

le_antisymm

Stable · empty-context checked

The witness-defined order is antisymmetric.

Exact expanded PA statement

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

Structural proof guide

The witness-defined order is antisymmetric.

Direct prerequisites: antisymm_from_witnesses. The authored body proceeds by case analysis (2).

Proof neighborhood

Direct dependencies

BT000I antisymm_from_witnesses

Direct dependents

BT00Q8 power_valuation_functional BT00QT prime_power_valuation_mul BT00WW bertrand_hj_base_window_thirty_two_from_total BT00YK no_bertrand_central_nonzero_valuation_factor_ranges

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