. exact div_nonneg hb (sqrt_nonneg π)
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π

case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)