BT001H

lt_trichotomy

Stable · empty-context checked

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

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

Direct prerequisites: none. The authored body proceeds by structural induction (3), case analysis (4), equality transport (2).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT004P beta_moduli_pairwise_coprime_bounded BT00PR prime_strictly_above_decidable BT00R2 ceil_div_six_functional BT00TJ choose_succ_succ

Formal native tactic body

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

  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