BT002B

multiple_mul_left

Stable · empty-context checked

A left multiple of a multiple remains a multiple.

Exact expanded PA statement

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

Structural proof guide

A left multiple of a multiple remains a multiple.

Direct prerequisites: mul_comm, multiple_mul_right. The authored body proceeds by equality transport (1).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT002A multiple_mul_right

Direct dependents

BT0101 prime_contribution_selected_successor_divides BT0102 prime_contribution_cofactor_prime_contradiction

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 n
  3. 0003intro m
  4. 0004intro hn
  5. 0005suffices hswap : m * n = n * m
  6. 0006rewrite hswap
  7. 0007apply multiple_mul_right
  8. 0008exact hn
  9. 0009apply mul_comm