BT0014

add_le_add_right

Stable · empty-context checked

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

Exact expanded PA statement

forall a b c. (exists k. k + a = b) -> exists r. r + (a + c) = b + c

Structural proof guide

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

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

Proof neighborhood

Direct dependencies

BT0003 add_assoc

Direct dependents

BT00R2 ceil_div_six_functional BT00RF ceil_div_six_le_of_upper BT00RG double_triple_remainder_complement_budget BT00WV bertrand_j_base_thirty_two_window_from_total BT00YA prime_square_tail_of_two_three_range BT00YB division_first_two_of_two_three_range BT010A two_lt_double_lower_six 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 + a) + c
  8. 0008symm
  9. 0009apply add_assoc
  10. 0010congr
  11. 0011exact h_witness
  12. 0012refl