BT001L

mul_le_mul_left

Stable · empty-context checked

Left multiplication 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

Left multiplication preserves the witness-defined order.

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

Proof neighborhood

Direct dependencies

BT0007 mul_add

Direct dependents

BT00PV mul_le_mul BT00PW le_mul_of_one_le_right BT00QE succ_le_mul_of_two_le_right BT00R2 ceil_div_six_functional BT00RC floor_sqrt_monotone BT00RF ceil_div_six_le_of_upper BT00RG double_triple_remainder_complement_budget BT00VK central_binom_strong_upper_step BT00X0 floor_sqrt_factorized_threshold_thirty_two BT00YA prime_square_tail_of_two_three_range BT00YF division_three_scaled_upper_of_quotient_lt BT00YH floor_sqrt_above_root_power_two_strict BT010E division_quotient_lower_of_scaled_le BT0115 bertrand_eventually_closed_upper BT0117 factor_pair_has_small_member_below_square

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 c * x
  7. 0007trans c * (x + a)
  8. 0008symm
  9. 0009apply mul_add
  10. 0010congr
  11. 0011refl
  12. 0012exact h_witness