PA000T

right_factor_divides_product

Stable checked-use theorem · independently closed

The right factor divides a product.

Exact expanded PA statement

forall a b. exists k. a * b = b * k

Structural proof guide

Generated structural guide

The right factor divides a product.

Use the direct prerequisites mul_comm as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000H mul_comm

Proof neighborhood

Direct dependencies

PA000H mul_comm

Direct dependents

PA001U beta_exclusive_accumulated_product_step

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. 0003exists a
  4. 0004apply mul_comm