English
Let r be a negative rational r = -n/d. Then ⌈r⌉ is the integer - ceil(n/d).
Русский
Пусть r — отрицательный рационал r = -n/d. Тогда ⌈r⌉ — целое число - ceil(n/d).
LaTeX
$$$$ \\text{If } r = -\\tfrac{n}{d}, \\lceil r \\rceil = -\\left\\lceil \\tfrac{n}{d} \\right\\rceil. $$$$
Lean4
theorem isInt_intCeil_ofIsRat_neg (r : α) (n : ℕ) (d : ℕ) : IsRat r (.negOfNat n) d → IsInt ⌈r⌉ (.negOfNat (n / d)) :=
by
rintro ⟨inv, rfl⟩
constructor
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
rw [@negOfNat_eq (n / d), ofNat_eq_coe, ← ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
floor_natCast_div_natCast n d, ← neg_neg (n : ℤ), ← ofNat_eq_coe, ← negOfNat_eq, ←
ceil_intCast_div_natCast (.negOfNat n) d, ← ceil_cast (α := α), Rat.cast_div, cast_intCast, cast_natCast]
