PA000G

mul_succ_left

Stable checked-use theorem · independently closed

A successor can move through multiplication on the left.

Exact expanded PA statement

forall n m. S n * m = n * m + m

Structural proof guide

Generated structural guide

A successor can move through multiplication on the left.

Use the direct prerequisites add_comm, add_assoc as previously established PA formulas.

The proof proceeds by structural induction (1), certified simplification (2).

Referenced ingredients

PA000F add_comm PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA000F add_comm PA0009 add_assoc

Direct dependents

PA000H mul_comm PA0025 mod_eq_predecessor_cancel PA002P base_le_beta_modulus PA0034 beta_half_range_entry_bounds PA005D predecessor_square_mod_one PA006Y odd_upper_remainder_reflection PA0070 gauss_pointwise_signed_half_representative PA007B gauss_mixed_sign_scaled_source_impossible PA007C gauss_signed_half_magnitude_injective PA00A2 prime_two_or_terminal_odd_shape PA00AG prime_bounded_square_one_cases PA00C2 odd_half_strictly_below_modulus PA00C4 predecessor_multiple_mod_complement PA00DQ odd_half_cross_product_gap PA00EK beta_repeat_sum_exact

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. 0002induction m
  3. 0003simp
  4. 0004specialize add_comm n
  5. 0005specialize add_comm m
  6. 0006simp [IH, add_comm, add_assoc]