use x, 1, 1 / y
x y z : ℝ
h : x * y * z = 1
⊢ ∃ a b c, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a / b ∧ y = b / c ∧ z = c / a
case h
x y z : ℝ
h : x * y * z = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x