Theorem: cycleMin_eq_fastCycleMin (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
i : ℕ
h : orderOf (π.cycleOf x) ≤ 2 ^ i
⊢ FastCycleMin i π x = CycleMin π x
Tactic:
rw [fastCycleMin_eq_min_cycleAtTo, cycleMin_eq_min_cycleAtTo_ge h]
State after:
no goals