English
Let l be a nodup list and view it as a cycle. Then the cycle is nontrivial iff its length is at least 2.
Русский
Пусть l — список без повторений. Превращая его в цикл, цикл тривиален тогда и только тогда, когда длина l не меньше 2.
LaTeX
$$$\operatorname{Nontrivial}(\Cycle.ofList(l)) \iff 2 \le \operatorname{length}(l)$, assuming $l$ is nodup.$$
Lean4
@[simp]
theorem nontrivial_coe_nodup_iff {l : List α} (hl : l.Nodup) : Nontrivial (l : Cycle α) ↔ 2 ≤ l.length :=
by
rw [Nontrivial]
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
· simp
· simp
· simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff, Nat.zero_le, iff_true]
refine ⟨hd, hd', ?_, by simp⟩
simp only [not_or, mem_cons, nodup_cons] at hl
exact hl.left.left
