English
For odd m and odd n and integers x,y, we have qrSign(m, n)·x = y if and only if x = qrSign(m, n)·y.
Русский
Для нечётных m и n и целых x,y верно qrSign(m, n)·x = y тогда и только тогда, когда x = qrSign(m, n)·y.
LaTeX
$$$\forall m,n \; (\text{Odd}(m) \land \text{Odd}(n)) \; \forall x,y \in \mathbb{Z},\ qrSign(m,n) \cdot x = y \iff x = qrSign(m,n) \cdot y$$$
Lean4
/-- We can move `qrSign m n` from one side of an equality to the other when `m` and `n` are odd. -/
theorem eq_iff_eq {m n : ℕ} (hm : Odd m) (hn : Odd n) (x y : ℤ) : qrSign m n * x = y ↔ x = qrSign m n * y := by
refine
⟨fun h' =>
let h := h'.symm
?_,
fun h => ?_⟩ <;>
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]