BT0013

le_add_right

Stable checked-use theorem · independently kernel verified

Adding on the right produces an explicit order witness.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

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

Structural proof guide

Adding on the right produces an explicit order witness.

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

Proof neighborhood

Direct dependencies

BT0002 add_comm

Direct dependents

BT0057 beta_value_lt_scaled_base BT00RG double_triple_remainder_complement_budget BT00UX primorial_factor_prefix_restrict_add BT00VV primorial_le_four_pow_bounded BT00X1 six_block_window_decomposition_above_thirty_two BT00X2 bertrand_hj_six_block_iterate_from_total BT00X4 bertrand_floor_power_product_le_h_from_total BT00Y5 central_binom_prime_power_contribution_le_double BT010H division_quotient_le_dividend BT010Q prime_contribution_prefix_restrict_add BT010V no_bertrand_small_contribution_choice_le_double

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

4 script commands · 3 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
add comm
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
02Construct an explicit witnessL3–3

Supply the displayed value, then prove that it has the required property.

  1. L3
    exists b
03Use earlier factsL4–4

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L4
    apply add_comm

Library-wide reading audit

Original exact command ledger · 4 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003exists b
  4. 0004apply add_comm