constructor
case h
x : ℝ
⊢ x ^ 2 = 17 ↔ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
case h.mp
x : ℝ
⊢ x ^ 2 = 17 → x = Real.sqrt 17 ∨ x = -Real.sqrt 17

case h.mpr
x : ℝ
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17 → x ^ 2 = 17