`BookProof.SmHiggsVacuum.higgsV_ge_min` {lam mu2 : ℝ} (hlam : 0 < lam) (phi : E) : -(mu2 ^ 2 / (4 * lam)) ≤ higgsV lam mu2 phi

Initializing...

`BookProof.SmHiggsVacuum.higgsV_ge_min` {lam mu2 : ℝ} (hlam : 0 < lam) (phi : E) : -(mu2 ^ 2 / (4 * lam)) ≤ higgsV lam mu2 phi · Prove2Me