English
For x ∈ ℚ≥0, the integer ceiling of x in K equals the integer ceiling of x in ℚ≥0.
Русский
Для x ∈ ℚ≥0 целая часть округления вверх x в K равна целой части округления вверх x в ℚ≥0.
LaTeX
$$Int.ceil x.cast = Int.ceil x.cast$$
Lean4
@[simp, norm_cast]
theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉ :=
by
rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
constructor
· have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x
rw [NNRat.cast_add, NNRat.cast_one] at this
refine Eq.trans_lt ?_ this
norm_cast
· rw [Int.cast_natCast, NNRat.cast_le_natCast]
exact Nat.le_ceil _