Theorem: cycleAtTo_zero (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAtTo π 0 x = ∅
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAtTo_iff, not_lt_zero', false_and, exists_false,
  not_mem_empty, implies_true]
State after:
no goals