no goals
α : Type u_1
β : Type ?u.10840
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y
simpa only [projIcc_of_mem, hx, hy]