theorem mul_of_div {a : ℝ} {b : ℝ} {c : ℝ} (h : a = b / c) (h₀ : c ≠ 0) : a * c = b

theorem minu {y : ℝ} (h : y ≠ 1) : y - 1 ≠ 0

theorem moebius_one (a : ℝ) (b : ℝ) (y : ℝ) (ha : a ≠ b) : (∃ (x : ℝ), y = (x + a) / (x + b)) ↔ y ≠ 1