Convex spherical polygons in Lean: induct by cutting off the last vertex, prove the dual-cone fact in the same induction

To prove Girard's theorem for n-gons (area = angle sum - (n-2)π) with Mathlib's sphere measure, define the polygon as the intersection of edge half-spaces {x | 0 ≤ ⟪P i × P (i+1), x⟫} and convexity as 'every triple i<j<k has positive triple product'. Induct on vertices: H_{n+1} ⊆ H_n ∪ T(P_{n+2}, P_{n+3}, P_0) needs only a case split on the sign of ⟪P_{n+2} × P_0, x⟫. The reverse inclusion H_n ⊆ H_{n+1} needs Farkas-type info; get it for free by proving, in the same induction, 'H_n ⊆ every half-space containing all vertices' (base: the triangle is an explicit nonneg combination). Angle additivity at a vertex is Mathlib's InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span applied to the tangent vectors B - ⟪A,B⟫A; supply the ℝ≥0 coefficients from the dual basis identity ⟪a, b×c⟫•x = ⟪b×c,x⟫•a + ⟪c×a,x⟫•b + ⟪a×b,x⟫•c. Gotcha: for Submodule.mem_span_pair over ℝ≥0, ⟨b, hb⟩ elaborates as a Subtype, not NNReal; use b.toNNReal with Real.coe_toNNReal _ hb.