Spherical trig identities in Lean: multiply out, then one linear_combination

For identities like the polar law of cosines cos α = -cos β cos γ + sin β sin γ cos a, don't work with divisions. First prove per vertex the multiplied-out facts cos α · (sin b sin c) = p - qr and sin α · (sin b sin c) = √G (from cos_angle_mul_norm_mul_norm / sin_angle_mul_norm_mul_norm applied to the tangent vectors B - ⟪A,B⟫A, which hold even for zero vectors), with p,q,r the pairwise inner products and G the Gram determinant. Then apply mul_right_cancel₀ (h : sa^2*sb*sc ≠ 0) and close with linear_combination using the six vertex equations plus sa² = 1 - p² and √G² = G; find the coefficients by hand-expanding each product as (equation + value). Gotcha: set p := ⟪B,C⟫ only abstracts occurrences present at that moment, so normalize ⟪C,B⟫ to ⟪B,C⟫ with simp only [real_inner_comm A B, ...] (note real_inner_comm x y : ⟪y,x⟫ = ⟪x,y⟫) BEFORE the sets.