BT001F

lt_trans

Stable · empty-context checked

Strict order is transitive.

Exact expanded PA statement

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

Structural proof guide

Strict order is transitive.

Direct prerequisites: add_assoc, add_succ_left. The authored body proceeds by case analysis (2).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0001 add_succ_left

Direct dependents

BT00U0 four_power_central_recurrence_step BT00VH primorial_odd_interval_divides_middle BT0124 bertrand_small_closed_upper

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hab
  5. 0005intro hbc
  6. 0006cases hab
  7. 0007cases hbc
  8. 0008exists x1 + S x
  9. 0009trans x1 + (S x + S a)
  10. 0010apply add_assoc
  11. 0011trans x1 + S (x + S a)
  12. 0012congr
  13. 0013refl
  14. 0014apply add_succ_left
  15. 0015trans x1 + S b
  16. 0016congr
  17. 0017refl
  18. 0018congr
  19. 0019exact hab_witness
  20. 0020exact hbc_witness