PA0011

lt_trichotomy

Stable checked-use theorem · independently closed

Two naturals are equal or strictly ordered in exactly one displayed direction.

Exact expanded PA statement

forall a b. a = b \/ ((exists k. k + S a = b) \/ exists k. k + S b = a)

Structural proof guide

Generated structural guide

Two naturals are equal or strictly ordered in exactly one displayed direction.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (3), case analysis (4), equality transport (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA001S beta_moduli_pairwise_coprime_bounded PA00D9 distinct_odd_prime_half_cell_oriented

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. 0001induction a
  2. 0002induction b
  3. 0003left
  4. 0004refl
  5. 0005right
  6. 0006left
  7. 0007exists b
  8. 0008trans S (b + 0)
  9. 0009apply PA4
  10. 0010congr
  11. 0011apply PA3
  12. 0012induction b
  13. 0013right
  14. 0014right
  15. 0015exists a
  16. 0016trans S (a + 0)
  17. 0017apply PA4
  18. 0018congr
  19. 0019apply PA3
  20. 0020specialize IH b
  21. 0021cases IH
  22. 0022left
  23. 0023congr
  24. 0024exact IH_left
  25. 0025cases IH_right
  26. 0026right
  27. 0027left
  28. 0028cases IH_right_left
  29. 0029exists x
  30. 0030rewrite PA4
  31. 0031congr
  32. 0032exact IH_right_left_witness
  33. 0033right
  34. 0034right
  35. 0035cases IH_right_right
  36. 0036exists x
  37. 0037rewrite PA4
  38. 0038congr
  39. 0039exact IH_right_right_witness