English
There is an induction principle for Cycle: to prove a property for all cycles it suffices to prove it for nil and to show that the property for a cycle formed by prepending any element to a smaller cycle follows from the property for that cycle.
Русский
Существует принцип индукции по Cycle: чтобы доказать свойство для всех циклов, достаточно доказать его для нуля и показать, что если свойство выполняется для некоторого цикла, то оно выполняется и для цикла, образованного добавлением элемента.
LaTeX
$$$\forall F:\\ Cycle\ α \to Prop,\ F(nil) \land (\forall a\ l, F(l) \to F(a::l)) \Rightarrow (\forall s:\ Cycle\ α, F(s))$$$
Lean4
/-- An induction principle for `Cycle`. Use as `induction s`. -/
@[elab_as_elim, induction_eliminator]
theorem induction_on {motive : Cycle α → Prop} (s : Cycle α) (nil : motive nil)
(cons : ∀ (a) (l : List α), motive ↑l → motive ↑(a :: l)) : motive s :=
Quotient.inductionOn' s fun l =>
by
refine List.recOn l ?_ ?_ <;> simp only [mk''_eq_coe, coe_nil]
assumption'
