no goals
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ (f^[n]) x ≤ (g^[n]) x ↔ f x ≤ g x
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)