no goals
R : Type u
S : Type v
A : Type w
B : Type ?u.536240
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) = (x - ↑(algebraMap R A) r) * x
rw [mul_sub, ← commutes, sub_mul]