English
For any integers num and den with den ≠ 0, and any x in an ordered additive group, mkRat num den ∈ ratLt x if and only if num·1 < den·x.
Русский
Для любых num ∈ ℤ и den ∈ ℕ с den ≠ 0 и любого x в упорядоченной аддитивной группе, mkRat num den ∈ ratLt x тогда и только тогда, когда num·1 < den·x.
LaTeX
$$$\\mathrm{mkRat}(\\mathrm{num}, \\mathrm{den}) \\in \\mathrm{ratLt}(x) \\iff \\mathrm{num} \\cdot 1 < \\mathrm{den} \\cdot x.$$$
Lean4
/-- Given `x` from `M`, one can informally write that, by transitivity,
`num / den ≤ x → x ≤ n → num / den ≤ n` for `den : ℕ` and `num n : ℕ`.
To avoid writing division for integer `num` and `den`, we express this in terms of
multiplication. -/
theorem num_le_nat_mul_den [ZeroLEOneClass M] [NeZero (1 : M)] {num : ℤ} {den : ℕ} {x : M} (h : num • 1 ≤ den • x)
{n : ℤ} (hn : x ≤ n • 1) : num ≤ n * den :=
by
refine le_of_smul_le_smul_right (h.trans ?_) (by simp)
rw [mul_comm, ← smul_smul]
simpa using nsmul_le_nsmul_right hn den
