PA003K

add_le_add_left

Stable checked-use theorem · independently closed

Adding the same left summand preserves the witness-defined order.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Adding the same left summand preserves the witness-defined order.

Use the direct prerequisites add_assoc, add_comm as previously established PA formulas.

The proof proceeds by case analysis (1).

Referenced ingredients

PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm

Direct dependents

PA007C gauss_signed_half_magnitude_injective PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

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 h
  5. 0005cases h
  6. 0006exists x
  7. 0007trans (x + c) + a
  8. 0008symm
  9. 0009apply add_assoc
  10. 0010trans (c + x) + a
  11. 0011congr
  12. 0012apply add_comm
  13. 0013refl
  14. 0014trans c + (x + a)
  15. 0015apply add_assoc
  16. 0016congr
  17. 0017refl
  18. 0018exact h_witness