PA0016

add_mul

Stable checked-use theorem · independently closed

Multiplication distributes over addition on the left.

Exact expanded PA statement

forall n m k. (n + m) * k = n * k + m * k

Structural proof guide

Generated structural guide

Multiplication distributes over addition on the left.

Use the direct prerequisites mul_comm, mul_add as previously established PA formulas.

The proof proceeds by certified simplification (1).

Referenced ingredients

PA000H mul_comm PA000A mul_add

Proof neighborhood

Direct dependencies

PA000H mul_comm PA000A mul_add

Direct dependents

PA0017 common_divisor_beta_moduli_divides_gap_times_c PA001J balanced_bezout_euclid_step PA001N balanced_combination_scale_right PA001Y mod_eq_mul_right PA002M mul_le_mul_right PA005N square_decomp PA006D odd_mul_odd PA00DQ odd_half_cross_product_gap

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 n
  2. 0002intro m
  3. 0003intro k
  4. 0004simp [mul_comm, mul_add]