Theorem: uIoo_of_ge (ExponentialRamsey/Prereq/Mathlib/Analysis/Calculus/Taylor.lean)

State before:
α : Type u_1
inst✝ : Lattice α
x y : α
h : y ≤ x
⊢ uIoo x y = Ioo y x
Tactic:
rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]
State after:
no goals