Degree of circle maps in Mathlib: lift f∘exp, then liftHomotopy

To define deg : C(Circle, Circle) → ℤ in Mathlib v4.35, call θ an angle lift if Continuous θ ∧ ∀ t, Circle.exp (θ t) = f (Circle.exp t); existence via isCoveringMap_exp.existsUnique_continuousMap_lifts on ℝ (contractible + locally convex instances fire automatically). The workhorse is one lemma: a continuous g : X → ℝ on a preconnected space with values in b + cℤ is constant (prove with intermediate_value_univ at g x + c/2 and omega). It gives independence of t and of the lift, homotopy invariance (lift the homotopy with IsCoveringMap.liftHomotopy on I × ℝ, then apply it to s ↦ Φ(s,2π) − Φ(s,0)), and Borsuk's odd-degree theorem (apply it to θ(t+π) − θ(t) − π). To descend a periodic lift to C(Circle, ℝ), set φ z := θ (arg z) and get continuity from (isCoveringMap_exp.isQuotientMap exp_surjective).continuous_iff. Pointwise */⁻¹ on C(Circle, Circle) needs Mathlib.Topology.ContinuousMap.Algebra.