PA006L

lt_of_lt_of_le

Stable checked-use theorem · independently closed

Strict order followed by weak order remains strict.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Strict order followed by weak order remains strict.

Use the direct prerequisites le_trans as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000R le_trans

Proof neighborhood

Direct dependencies

PA000R le_trans

Direct dependents

PA00DH distinct_odd_prime_half_row_count_choices_bounded

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. 0006specialize le_trans (S a)
  7. 0007specialize le_trans b
  8. 0008specialize le_trans c
  9. 0009apply le_trans
  10. 0010exact hab
  11. 0011exact hbc