PA0033

lt_of_le_of_lt

Stable checked-use theorem · independently closed

Weak order followed by strict order remains strict.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Weak order followed by strict order remains strict.

Use the direct prerequisites add_assoc as previously established PA formulas.

The proof proceeds by case analysis (2), equality transport (2).

Referenced ingredients

PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA0009 add_assoc

Direct dependents

PA0034 beta_half_range_entry_bounds PA007C gauss_signed_half_magnitude_injective PA00AG prime_bounded_square_one_cases PA00C6 odd_signed_division_branch_exact PA00D8 distinct_odd_prime_half_products_ne PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero PA00DS nonzero_remainder_division_positive_multiple_threshold

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 a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hab
  5. 0005intro hbc
  6. 0006cases hab
  7. 0007cases hbc
  8. 0008exists x1 + x
  9. 0009trans x1 + (x + S a)
  10. 0010apply add_assoc
  11. 0011rewrite PA4
  12. 0012rewrite hab_witness
  13. 0013exact hbc_witness