PA002S

le_add_right

Stable checked-use theorem · independently closed

Adding on the right produces an explicit order witness.

Exact expanded PA statement

forall a b. exists k. k + a = a + b

Structural proof guide

Generated structural guide

Adding on the right produces an explicit order witness.

Use the direct prerequisites add_comm as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000F add_comm

Proof neighborhood

Direct dependencies

PA000F add_comm

Direct dependents

PA002T beta_value_lt_scaled_base PA00DR odd_half_division_quotient_bounded

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. 0003exists b
  4. 0004apply add_comm