no goals
α : Type u_1
β : Type ?u.8358
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
rw [add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]
no goals
α : Type u_1
β : Type ?u.8358
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
ha.assoc]