no goals
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : ↑f x ≤ x + ↑m
n : ℕ
⊢ (↑f^[n]) x ≤ x + ↑n * ↑m
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_le_of_map_le f.monotone (monotone_id.add_const (m : ℝ)) h n