suffices |t| < N + 1 by linarith [(by exact_mod_cast (by omega) : 1 ≤ (N : ℝ))]
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| ≤ 2 * ↑N
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| < ↑N + 1