PA000C

multiple_mul_right

Stable checked-use theorem · independently closed

A right multiple of a multiple remains a multiple.

Exact expanded PA statement

forall a n m. (exists q. n = a * q) -> exists s. n * m = a * s

Structural proof guide

Generated structural guide

A right multiple of a multiple remains a multiple.

Use the direct prerequisites mul_assoc as previously established PA formulas.

The proof proceeds by case analysis (1), equality transport (1).

Referenced ingredients

PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA000B mul_assoc

Direct dependents

PA000I bounded_common_multiple_step PA000L scaled_bounded_common_multiple PA001U beta_exclusive_accumulated_product_step PA008M quadratic_residue_half_power_mod_one

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 n
  3. 0003intro m
  4. 0004intro hn
  5. 0005cases hn
  6. 0006exists x * m
  7. 0007rewrite hn_witness
  8. 0008apply mul_assoc