constructor
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A → x = (A / 2) ^ 2 + 1 / 2

case mpr
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ x = (A / 2) ^ 2 + 1 / 2 → IsGood x A