English
If n > 2, then for any i, j ∈ Fin(n) with i ≠ j, there exists k ∈ Fin(n) with k ≠ i and k ≠ j.
Русский
Если n > 2, то для любых i, j ∈ Fin(n) с i ≠ j существует k ∈ Fin(n) такое, что k ≠ i и k ≠ j.
LaTeX
$$$$\forall i,j:\\mathrm{Fin}(n),\ i\neq j\ \\Rightarrow\ \exists k:\\mathrm{Fin}(n),\ k\neq i \land k\neq j.$$$$
Lean4
/-- If working with more than two elements, we can always pick a third distinct from two existing
elements. -/
theorem exists_ne_and_ne_of_two_lt (i j : Fin n) (h : 2 < n) : ∃ k, k ≠ i ∧ k ≠ j :=
by
have : NeZero n := ⟨by cutsat⟩
rcases i with ⟨i, hi⟩
rcases j with ⟨j, hj⟩
simp_rw [← Fin.val_ne_iff]
by_cases h0 : 0 ≠ i ∧ 0 ≠ j
· exact ⟨0, h0⟩
· by_cases h1 : 1 ≠ i ∧ 1 ≠ j
· exact ⟨⟨1, by cutsat⟩, h1⟩
· refine ⟨⟨2, by cutsat⟩, ?_⟩
dsimp only
cutsat
