PA006M

mul_le_mul_left

Stable checked-use theorem · independently closed

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

Generated structural guide

Left multiplication preserves the witness-defined order.

Use the direct prerequisites mul_add as previously established PA formulas.

The proof proceeds by case analysis (1).

Referenced ingredients

PA000A mul_add

Proof neighborhood

Direct dependencies

PA000A mul_add

Direct dependents

PA00DR odd_half_division_quotient_bounded PA00DS nonzero_remainder_division_positive_multiple_threshold

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  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