no goals
S : Type ?u.171562
R : Type u_1
R₁ : Type ?u.171568
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y y' : M
⊢ polar (↑Q) x (y - y') = polar (↑Q) x y - polar (↑Q) x y'
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]