Nat_Mult_Comm_Lemma
Proveda * (b+1) = a*b + a.
Preamble
import Mathlib.Tactic
Formal statement
theorem Nat_Mult_Comm_Lemma (a b : ℕ) : a * (b + 1) = a * b + a := by sorry
a * (b+1) = a*b + a.
import Mathlib.Tactic
theorem Nat_Mult_Comm_Lemma (a b : ℕ) : a * (b + 1) = a * b + a := by sorry