BT0013

le_add_right

Stable · empty-context checked

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

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 this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

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