English
Let R be a ring with a linear order, a strict ordered ring, and a FloorRing. If r is a natural number, then its floor is the same natural number; i.e. IsNat r m implies IsNat ⌊r⌋ m.
Русский
Пусть R — кольцо с линейным порядком, строгим упорядоченным кольцом и FloorRing. Если r натуральное число, то ⌊r⌋ равно этому же натуральному числу; то есть IsNat r m → IsNat ⌊r⌋ m.
LaTeX
$$$$ \\text{IsNat } r\, m \\;\\rightarrow\\; \\text{IsNat } \\lfloor r \\rfloor\, m, \\quad r \\in R,\\; m \\in \\mathbb{N}. $$$$
Lean4
theorem isNat_intFloor {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℕ) :
IsNat r m → IsNat ⌊r⌋ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩
