PA000G

mul_succ_left

Stable checked-use theorem · independently closed

A successor can move through multiplication on the left.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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.

Read the argument

Proof checkpoints

6 script commands · 2 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
add comm
01Fix variables and assumptionsL1–1

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
02Induction on mL2–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction m
  2. L3
    simp
  3. L4
    specialize add_comm n
  4. L5
    specialize add_comm m
  5. L6
    simp [IH, add_comm, add_assoc]

Library-wide reading audit

Original exact command ledger · 6 lines
  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]