PA006T

odd_half_unique

Stable checked-use theorem · independently closed

The half witness in an odd decomposition is unique.

Exact expanded PA statement

forall n a b. n = 2 * a + 1 -> n = 2 * b + 1 -> a = b

Structural proof guide

Generated structural guide

The half witness in an odd decomposition is unique.

Use the direct prerequisites add_right_cancel, mul_left_cancel_nonzero as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA0012 add_right_cancel PA006S mul_left_cancel_nonzero

Proof neighborhood

Direct dependencies

PA0012 add_right_cancel PA006S mul_left_cancel_nonzero

Direct dependents

PA00FI odd_half_of_mod4_one_exact PA00FQ odd_half_of_mod4_three_exact

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 n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro ha
  5. 0005intro hb
  6. 0006have hs : 2 * a + 1 = 2 * b + 1
  7. 0007trans n
  8. 0008symm
  9. 0009exact ha
  10. 0010exact hb
  11. 0011have hm : 2 * a = 2 * b
  12. 0012specialize add_right_cancel (2 * a)
  13. 0013specialize add_right_cancel (2 * b)
  14. 0014specialize add_right_cancel 1
  15. 0015apply add_right_cancel
  16. 0016exact hs
  17. 0017specialize mul_left_cancel_nonzero 2
  18. 0018specialize mul_left_cancel_nonzero a
  19. 0019specialize mul_left_cancel_nonzero b
  20. 0020apply mul_left_cancel_nonzero
  21. 0021intro htwo
  22. 0022apply PA1
  23. 0023exact htwo
  24. 0024exact hm