let c' : Set.Icc 1 m → Fin 2 :=
  fun x ↦ c ⟨x.val, by rw [Set.mem_Icc]; exact ⟨x.prop.1, x.prop.2.trans hmn⟩⟩
case right
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
⊢ coloring_is_good c
case right
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
c' : ↑(Set.Icc 1 m) → Fin 2 := fun x => c ⟨↑x, ⋯⟩
⊢ coloring_is_good c