BT0015

add_le_add_left

Stable · empty-context checked

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

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

Direct prerequisites: add_assoc, add_comm. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm

Direct dependents

BT00R1 ceil_div_six_total BT00RI floor_ceil_complement_budget BT00UW primorial_interval_factor_prefix_shift BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle BT00X1 six_block_window_decomposition_above_thirty_two BT00YA prime_square_tail_of_two_three_range BT00YB division_first_two_of_two_three_range BT010A two_lt_double_lower_six BT010P prime_contribution_interval_prefix_shift BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT011Q bertrand_covering_interval

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. 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