case zero
h : 0 < Nat.zero
⊢ cycleRange { val := 0, isLt := h } = 1

case succ
n : ℕ
h : 0 < Nat.succ n
⊢ cycleRange { val := 0, isLt := h } = 1
n : ℕ
h : 0 < n
⊢ cycleRange { val := 0, isLt := h } = 1
cases' n with n
no goals
case succ
n : ℕ
h : 0 < Nat.succ n
⊢ cycleRange { val := 0, isLt := h } = 1
exact cycleRange_zero n
no goals
case zero
h : 0 < Nat.zero
⊢ cycleRange { val := 0, isLt := h } = 1
cases h