BT001M

mul_le_mul_right

Stable · empty-context checked

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

Right multiplication preserves the witness-defined order.

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

Proof neighborhood

Direct dependencies

BT000B add_mul

Direct dependents

BT0055 le_scaled_nonzero BT00PV mul_le_mul BT00PX le_mul_of_one_le_left BT00R9 square_lt_successor_square BT00RC floor_sqrt_monotone BT00RG double_triple_remainder_complement_budget BT00TY mul_lt_mul_right_nonzero BT00VK central_binom_strong_upper_step BT00X6 bertrand_main_inequality_factorized_from_total BT00YH floor_sqrt_above_root_power_two_strict BT010C three_mul_le_square_of_three_le 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 x * c
  7. 0007trans (x + a) * c
  8. 0008symm
  9. 0009apply add_mul
  10. 0010congr
  11. 0011exact h_witness
  12. 0012refl