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