chore(linear_algebra/quadratic_form): add two missing simp lemmas about subtraction (#5985)
chore(linear_algebra/quadratic_form): add two missing simp lemmas about subtraction (#5985)

This also reorders the instance definitions to keep the lemmas about subtraction near the ones about negation, and uses the `add := (+)` pattern to make definitions unfold more nicely, even though it probably doesn't make any difference.






leanprover-community/mathlib,leanprover-community/mathlib