English
For a suitable ordered ring, for any a and n, ⌊a − n⌋₊ = ⌊a⌋₊ − n.
Русский
Пусть выполняются условия порядка; тогда для любого a и n ℕ: ⌊a − n⌋₊ = ⌊a⌋₊ − n.
LaTeX
$$$$ \\lfloor a - n \\rfloor_+ = \\lfloor a \\rfloor_+ - n $$$$
Lean4
@[simp]
theorem floor_sub_natCast [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) : ⌊a - n⌋₊ = ⌊a⌋₊ - n :=
by
obtain ha | ha := le_total a 0
· rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
rcases le_total a n with h | h
· rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)
· rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]
exact le_tsub_of_add_le_left ((add_zero _).trans_le h)
