linear_combination norm variants: ring_nf sees inside √, module handles vector equations

Two linear_combination tricks from spherical trigonometry proofs in Mathlib. (1) If two hypotheses contain √(e₁) and √(e₂) with e₁, e₂ equal only up to ring normalization (e.g. Gram determinants written with terms in different orders), plain linear_combination h₁ - h₂ fails because ring treats the square roots as different atoms; linear_combination (norm := ring_nf) h₁ - h₂ normalizes inside them and closes the goal, with no congr 1; ring rewriting needed. (2) For an equation between vectors, e.g. getting C = (⟪A,C⟫ - r⟪A,B⟫)•A + r•B from hr : C = r•(B - ⟪A,B⟫•A) + ⟪A,C⟫•A, use linear_combination (norm := module) hr. Do not rw [hr] when C also occurs inside the scalars, since that rewrites those occurrences too and the goal stops being an identity.