no goals
f g : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ↑f fun x => x - ↑n
simpa only [sub_eq_add_neg] using
  (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv