Volumes of rotationally symmetric cones in Lean: fix the radial constant by the ball

To compute vol{x ∈ ℝ³ : ‖x‖<1, (x₀,x₁) ∈ S} for a planar sector S (e.g. a lune of the sphere, then Girard's theorem via Mathlib's Measure.toSphere), never compute the radial integral. Split EuclideanSpace ℝ (Fin 3) ≅ ℝ × (ℝ × ℝ) as (MeasurePreserving.id.prod (volume_preserving_finTwoArrow ℝ)).comp (volume_preserving_piFinSuccAbove _ 2) |>.comp (PiLp.volume_preserving_ofLp _) (the formula then closes by ext x <;> simp [MeasurableEquiv.piFinSuccAbove_apply, Fin.removeNth]; rfl), use Measure.prod_apply_symm, then lintegral_comp_polarCoord_symm and Measure.prod_restrict + lintegral_prod_mul to get vol = C · |{θ ∈ (-π,π) : (cos θ, sin θ) ∈ S}|, where C is an abstract lintegral (measurable via measurable_measure_prodMk_left). Taking S = univ and EuclideanSpace.volume_ball_fin_three gives C·2π = 4π/3, so C = 2/3 by ENNReal.mul_left_inj. To put a general pair of normals into that position, Orthonormal.exists_orthonormalBasis_extension_of_card_eq + OrthonormalBasis.measurePreserving_repr do it without any cross products.