English
There exists a 3-coloring of a cycle graph for n ≥ 2.
Русский
Существует трёхцветное раскраска цикла графа для n ≥ 2.
LaTeX
$$cycleGraph.tricoloring (n) (h) : Coloring (cycleGraph n) (Fin 3)$$
Lean4
/-- Tricoloring of a cycle graph -/
def tricoloring (n : ℕ) (h : 2 ≤ n) : Coloring (cycleGraph n) (Fin 3) :=
Coloring.mk (fun u ↦ if u.val = n - 1 then 2 else ⟨u.val % 2, by fin_omega⟩) <|
by
intro u v hadj
match n with
| 0 => exact u.elim0
| 1 => simp at h
| n + 2 =>
simp only
simp only [cycleGraph_adj] at hadj
split_ifs with hu hv
· simp [Fin.eq_mk_iff_val_eq.mpr hu, Fin.eq_mk_iff_val_eq.mpr hv] at hadj
· refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm
exact v.val.mod_lt Nat.zero_lt_two
· refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))
exact u.val.mod_lt Nat.zero_lt_two
· simp only [ne_eq, Fin.ext_iff]
have hu' : u.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
have hv' : v.val + (1 : Fin (n + 2)) < n + 2 := by fin_omega
cases hadj with
| inl huv
| inr huv =>
rw [← add_eq_of_eq_sub' huv.symm]
simp only [Fin.val_add_eq_of_add_lt hv', Fin.val_add_eq_of_add_lt hu', Fin.val_one]
rw [show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; cutsat, Nat.even_add]
simp only [Nat.not_even_one, iff_false, not_iff_self, iff_not_self]
exact id