English
There is a divisor-case elimination principle for rationals: every q can be represented as n/d with d > 0 and gcd(|n|, d) = 1, and a selector div describes the value on that representation.
Русский
Существует принцип разложения рационального числа на дробь с НОДом 1: q = n/d, где d > 0 и gcd(|n|, d) = 1, и заданная функция div определяет значение для такого представления.
LaTeX
$$$\exists n \in \mathbb{Z}, \exists d \in \mathbb{N}, d \neq 0 \land n.natAbs.Coprime d \land a = n/d$$$
Lean4
/-- A version of `Rat.casesOn` that uses `/` instead of `Rat.mk'`. Use as
```lean
cases r with
| div p q nonzero coprime =>
```
-/
@[elab_as_elim, cases_eliminator, induction_eliminator]
def divCasesOn {C : ℚ → Sort*} (a : ℚ) (div : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → n.natAbs.Coprime d → C (n / d)) : C a :=
a.casesOn fun n d nz red => by rw [Rat.mk'_eq_divInt, Rat.divInt_eq_div]; exact div n d nz red
