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

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