Is Bounded 𝓵 nonneg

lemma isBounded_𝓵_nonneg (h : P.IsBounded) : 0 ≤ P.𝓵 := by  by_contra hl  rw [not_le] at hl  obtain ⟨c, hc⟩ := h  have c_le_of_attainable : ∀ v : ℝ, ((0 < P.μ2 ∧ v ≤ 0) ∨      (P.μ2 ≤ 0 ∧ v ≤ - P.μ2 ^ 2 / (4 * P.𝓵))) → c ≤ v := by    intro v hv    obtain ⟨φ, x, rfl⟩ := (P.neg_𝓵_sol_exists_iff hl v).mpr hv    exact hc φ x  by_cases hμ : P.μ2 ≤ 0  · by_cases hcz : c ≤ - P.μ2 ^ 2 / (4 * P.𝓵)    · linarith [c_le_of_attainable (c - 1) (Or.inr ⟨hμ, by linarith⟩)]    · rw [not_le] at hcz      linarith [c_le_of_attainable (- P.μ2 ^ 2 / (4 * P.𝓵) - 1) (Or.inr ⟨hμ, by linarith⟩)]  · rw [not_le] at hμ    by_cases hcz : c ≤ 0    · linarith [c_le_of_attainable (c - 1) (Or.inl ⟨hμ, by linarith⟩)]    · rw [not_le] at hcz      linarith [c_le_of_attainable 0 (Or.inl ⟨hμ, by linarith⟩)]