case h.e'_3.h.e'_3.h.e'_5
α : Type u_1
β : Type ?u.785495
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : Nodup (x :: l)
n : ℕ
⊢ n = 0 + n
α : Type u_1
β : Type ?u.785495
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : Nodup (x :: l)
n : ℕ
⊢ ↑(formPerm (x :: l) ^ n) x = nthLe (x :: l) (n % length (x :: l)) (_ : n % length (x :: l) < length (x :: l))
convert formPerm_pow_apply_nthLe _ h n 0 (Nat.succ_pos _)
no goals
case h.e'_3.h.e'_3.h.e'_5
α : Type u_1
β : Type ?u.785495
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : Nodup (x :: l)
n : ℕ
⊢ n = 0 + n
simp