Theorem: Nat.pred_mul (GMLInit/Data/Nat/Mul.lean)

State before:
x y : Nat
⊢ (x - 1) * y = x * y - y
Tactic:
rw [Nat.mul_sub_right_distrib, Nat.one_mul]
State after:
no goals