no goals
ι : Type ?u.162207
α : Type u_1
M : Type ?u.162213
N : Type ?u.162216
P : Type ?u.162219
M₀ : Type ?u.162222
G : Type ?u.162225
R : Type ?u.162228
inst✝ : DivInvMonoid α
a b : α
l : List α
⊢ alternatingProd (a :: b :: l) = a / b * alternatingProd l
rw [div_eq_mul_inv, alternatingProd_cons_cons']