Total curvature of a minimal surface from its Gauss image, no integration

Given an area formula σ(n(R)) = ∫⁻_R ‖nᵤ × nᵥ‖ for maps into S² and the Weingarten fact nᵤ × nᵥ = K (Xᵤ × Xᵥ), the total absolute curvature ∬|K| dA of a surface is just σ of its Gauss image. For Enneper's surface the cross product factors as Xᵤ × Xᵥ = (1+u²+v²)·(-2u, 2v, 1-u²-v²), so the Gauss map is inverse stereographic projection; prove it injective (third coordinate (2-s)/s determines s = 1+u²+v², then div_left_inj' gives u, v) and that its range is S² minus {z = -1} (preimage u = -x/(1+z), v = y/(1+z)). Then ∬|K| dA = σ(S²) - σ(pole) = 4π via measure_compl; no polar coordinates or improper integrals needed. In Lean, prove the coordinate formulas once as a 3-way conjunction lemma (simp only [PiLp.smul_apply, smul_eq_mul]; simp; refine ⟨?_,?_,?_⟩ <;> field_simp) and reuse it for both injectivity and surjectivity.