English
If the natural-number threshold comparisons agree between a in R and b in S, then the floors are equal: ⌊a⌋ = ⌊b⌋.
Русский
Если сравнения по порогам натуральных чисел совпадают для a и b, то округления равны: ⌊a⌋ = ⌊b⌋.
LaTeX
$$$$ \\forall n, (n \\le a) \\iff (n \\le b) \\Rightarrow \\lfloor a \\rfloor = \\lfloor b \\rfloor $$$$
Lean4
theorem floor_congr [IsStrictOrderedRing R] [IsStrictOrderedRing S] (h : ∀ n : ℕ, (n : R) ≤ a ↔ (n : S) ≤ b) :
⌊a⌋₊ = ⌊b⌋₊ := by
have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
obtain ha | ha := lt_or_ge a 0
· rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)]
exact (le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)
