English
Let a be a nonnegative element of a linearly ordered ring equipped with a floor operation that lands in natural numbers. Then for every natural n, the floor of a plus n (viewed in the ambient ring) equals the floor of a plus n: ⌊a + n⌋₊ = ⌊a⌋₊ + n.
Русский
Пусть a ≥ 0 в линейно упорядоченной части кольца, на котором задана целая часть, и пусть n ∈ ℕ. Тогда ⌊a + n⌋₊ = ⌊a⌋₊ + n.
LaTeX
$$$$ \\lfloor a + n \\rfloor_+ = \\lfloor a \\rfloor_+ + n $$$$
Lean4
theorem floor_add_natCast [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) : ⌊a + n⌋₊ = ⌊a⌋₊ + n :=
eq_of_forall_le_iff fun b => by
rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]
obtain hb | hb := le_total n b
· obtain ⟨d, rfl⟩ := exists_add_of_le hb
rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right, le_floor_iff ha]
· obtain ⟨d, rfl⟩ := exists_add_of_le hb
rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
refine iff_of_true ?_ le_self_add
exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg
