`BookProof.LimitCircleExample.lcSol_sq_le` (x : ℝ) : ‖lcSol x‖ ^ 2 ≤ Real.exp π * (1 + x ^ 2)⁻¹

Initializing...

`BookProof.LimitCircleExample.lcSol_sq_le` (x : ℝ) : ‖lcSol x‖ ^ 2 ≤ Real.exp π * (1 + x ^ 2)⁻¹ · Prove2Me