Pigeonhole on arguments of unit complex numbers in Lean: clamp the floor

For simultaneous Dirichlet approximation (find y ≠ 0 with |ψ y - 1| ≤ 2π/M for all characters ψ ∈ Λ), index arcs by min ⌊(Complex.arg z + π) * M / (2 * π)⌋₊ (M - 1). arg lies in (-π, π], so the unclamped floor can equal M at arg = π; the min puts that point in the last arc. Both cases still give k ≤ u ≤ k + 1, so no special case is needed. Then use Finset.exists_ne_map_eq_of_card_lt_of_maps_to into Fintype.piFinset fun _ : Λ ↦ range M, write unit z as Complex.exp (I * arg z) from Complex.norm_mul_exp_arg_mul_I, and finish with Real.norm_exp_I_mul_ofReal_sub_one_le (namespace Real, not Complex). For |z^j - 1| ≤ j|z - 1|, induct with z^(j+1) - 1 = z^j (z - 1) + (z^j - 1).