English
Let R be a ring with linear order, IsStrictOrderedRing, FloorRing. If r is NN rational with representation (n/d), then ⌈r⌉ is a natural number equal to the natural Ceil(n/d).
Русский
Пусть R — кольцо с линейным порядком, IsStrictOrderedRing и FloorRing. Если r — NN рационал с представлением (n/d), то ⌈r⌉ является натуральным числом, равным ceil(n/d).
LaTeX
$$$$ \\text{IsNNRat } r\\ n\\ d \\rightarrow \\text{IsNat } \\lceil r \\rceil \\ (-(-n/d):\\mathbb{Z}).toNat. $$$$
Lean4
theorem isNat_intCeil_ofIsNNRat (r : α) (n : ℕ) (d : ℕ) : IsNNRat r n d → IsNat ⌈r⌉ (-(-n / d) : ℤ).toNat :=
by
rintro ⟨inv, rfl⟩
constructor
simp only [invOf_eq_inv, ← div_eq_mul_inv]
rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div, cast_intCast, cast_natCast, Int.cast_natCast,
Int.natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg))]
