rw [Set.mem_Icc]
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
x : ↑(Set.Icc 1 m)
⊢ ↑x ∈ Set.Icc 1 n
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
x : ↑(Set.Icc 1 m)
⊢ 1 ≤ ↑x ∧ ↑x ≤ n