BT002A

multiple_mul_right

Stable · empty-context checked

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

A right multiple of a multiple remains a multiple.

Direct prerequisites: mul_assoc. The authored body proceeds by case analysis (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT0008 mul_assoc

Direct dependents

BT002B multiple_mul_left BT004M bounded_common_multiple_step BT0056 scaled_bounded_common_multiple BT0059 beta_exclusive_accumulated_product_step BT0069 beta_factor_divides_product

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. 0005cases hn
  6. 0006exists x * m
  7. 0007rewrite hn_witness
  8. 0008apply mul_assoc