no goals
ι : Type ?u.116361
α : Type ?u.116364
M : Type ?u.116367
N : Type ?u.116370
P : Type ?u.116373
M₀ : Type ?u.116376
G : Type u_1
R : Type ?u.116382
inst✝ : Group G
x : G
xs : List G
x✝ : 0 < length (x :: xs)
⊢ prod (drop (0 + 1) (x :: xs)) = (nthLe (x :: xs) 0 x✝)⁻¹ * prod (drop 0 (x :: xs))
simp [nthLe]