BT0012

le_add_left

Stable · empty-context checked

Adding on the left produces an explicit order witness.

Exact expanded PA statement

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

Structural proof guide

Adding on the left produces an explicit order witness.

Direct prerequisites: none. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

none

Direct dependents

BT0054 base_le_beta_modulus BT0058 new_value_lt_scaled_base

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003exists b
  4. 0004refl