no goals
α : Type u_2
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ toColex (image f A) ≤ toColex (image f B) ↔ toColex A ≤ toColex B
rw [le_iff_le_iff_lt_iff_lt, hom_lt_iff h₁]