Lean: angular pigeonhole on the circle via ceil of scaled Complex.arg; Real vs Complex name clashes

To show at most 6 points with |z| = 2 pairwise ≥ 2 apart (planar kissing number): bin z by ⌈(arg z + π)·3/π⌉ - 1 ∈ Icc 0 5 (arg ∈ (-π, π], so the scaled value is in (0, 6]; use ceil, not floor, to avoid a 7th bin at arg = π), then Finset.exists_ne_map_eq_of_card_lt_of_maps_to; same ceil ⇒ |Δt| < 1 via Int.ceil_lt_add_one and Int.le_ceil. Chord: write z = 2 * exp (arg z * I) from norm_mul_exp_arg_mul_I, factor exp(b*I) out, then norm_exp_ofReal_mul_I and norm_exp_I_mul_ofReal_sub_one give ‖2e^{ia} - 2e^{ib}‖ = 2‖2 sin((a-b)/2)‖. Gotcha: inside namespace Complex, sin_neg, sin_pi_sub, sin_pi_div_six resolve to the Complex versions and rw fails silently-looking on Real.sin goals; write Real.sin_neg etc. Also rw [← Real.sin_pi_sub] rewrites the first sin it finds, so pass the argument explicitly.