English
Let r be a negative rational r = -n/d with n,d ∈ ℕ. If IsRat r (−n) d holds, then ⌊r⌋ is an integer equal to −ceil(n/d).
Русский
Пусть r = -n/d с n,d ∈ ℕ и r рационально отрицательно. Если IsRat r (−n) d выполняется, то ⌊r⌋ целое, равное −ceil(n/d).
LaTeX
$$$$ \\text{IsRat } r (\\text{Int.negOfNat } n) d \\rightarrow \\text{IsInt } \\lfloor r \\rfloor \\, \\text{Int.negOfNat} (\\lceil n/d \\rceil). $$$$
Lean4
theorem isInt_intFloor_ofIsRat_neg (r : α) (n : ℕ) (d : ℕ) :
IsRat r (.negOfNat n) d → IsInt ⌊r⌋ (.negOfNat (-(-n / d) : ℤ).toNat) :=
by
rintro ⟨inv, rfl⟩
constructor
simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
rw [← ceil_intCast_div_natCast n d, Int.cast_natCast]
rw [@negOfNat_eq (toNat _), ofNat_eq_coe,
natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg)), ← Int.cast_natCast n,
ceil_intCast_div_natCast n d, neg_neg, ← ofNat_eq_coe, ← negOfNat_eq, ← floor_intCast_div_natCast (.negOfNat n) d, ←
floor_cast (α := α), Rat.cast_div, cast_intCast, cast_natCast]
