Lean: glue two arcs on [0,1] into a circle map with Continuous.if_le

To turn two arcs α, β : ℝ → ℂ with equal endpoints into a closed curve, use g t = if t ≤ π then α (t/π) else β (2 - t/π). Assume α, β are continuous on all of ℝ (precompose with projIcc if needed). Then Continuous.if_le (hα.comp _) (hβ.comp _) continuous_id continuous_const gives global continuity; the agreement goal at t = π is α 1 = β 1. Then lift to the circle via AddCircle.liftIco + homeomorphCircle'. Gotcha in the range proof: the preimage of a point β c is (2 - c)π only for c < 1. At c = 1 the t ≤ π branch fires, so treat c = 0, c = 1 and 0 < c < 1 separately (eq_or_lt_of_le twice).