no goals
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f^[n]) x < x + ↑n * ↑m ↔ ↑f x < x + ↑m
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_lt_iff_map_lt f.monotone (strictMono_id.add_const (m : ℝ)) hn