The ceiling of a quotient, and of small rationals

Candidates for Mathlib.Data.Rat.Floor: the ceiling of n / d for an integer n and a positive natural number d is (n + d - 1) / d (Rat.ceil_intCast_div_natCast_eq_add_sub_one_div), the form next to Rat.ceil_intCast_div_natCast that rounds up by the integer division; and two nonzero rationals strictly between -1 and 1 of the same sign have the same ceiling and the same floor (Rat.ceil_eq_and_floor_eq_of_abs_lt_one).

Main statements

• Rat.ceil_intCast_div_natCast_eq_add_sub_one_div: ⌈n / d⌉ = (n + d - 1) / d for d > 0.
• Rat.ceil_eq_and_floor_eq_of_abs_lt_one: the ceilings and the floors of two nonzero rationals of the same sign strictly between -1 and 1.

theorem Rat.ceil_intCast_div_natCast_eq_add_sub_one_div (n : ℤ) {d : ℕ} (hd : 0 < d) : ⌈↑n / ↑d⌉ = (n + ↑d - 1) / ↑d

The ceiling of n / d for d > 0 by the integer division, rounded up: (n + d - 1) / d, where Rat.ceil_intCast_div_natCast has -((-n) / d) for every d.

theorem Rat.ceil_eq_and_floor_eq_of_abs_lt_one {p p' : ℚ} (hp : p ≠ 0) (hp1 : |p| < 1) (hp' : p' ≠ 0) (hp1' : |p'| < 1) (hs : p < 0 ↔ p' < 0) : ⌈p⌉ = ⌈p'⌉ ∧ ⌊p⌋ = ⌊p'⌋

Two nonzero rationals of the same sign strictly between -1 and 1 have the same ceiling and the same floor: 1 and 0 when positive, 0 and -1 when negative.