no goals
x : ℝ
⊢ 0 ≤ expNegInvGlue x
cases le_or_gt x 0 with
| inl h => exact ge_of_eq (zero_of_nonpos h)
| inr h => exact le_of_lt (pos_of_pos h)
no goals
case inl
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x
exact ge_of_eq (zero_of_nonpos h)
no goals
case inr
x : ℝ
h : x > 0
⊢ 0 ≤ expNegInvGlue x
exact le_of_lt (pos_of_pos h)