BT0005

mul_succ_left

Stable · empty-context checked

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

A successor can move through multiplication on the left.

Direct prerequisites: add_comm, add_assoc. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT0003 add_assoc

Direct dependents

BT0006 mul_comm BT0024 two_large_factors_impossible BT004E mod_eq_predecessor_cancel BT0054 base_le_beta_modulus BT006N prime_three BT00TT choose_weighted_vertical BT00UE primorial_positive BT00YF division_three_scaled_upper_of_quotient_lt BT011K prime_eighty_three

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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]