rw [mul_tsub, mul_one]
α : Type u_1
inst✝⁴ : CanonicallyOrderedCommSemiring α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b - 1) = a * b - a
no goals