have h := integral_gaussian
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-b * x ^ 2) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1