ctx : Context
p : Poly
k : Nat
m : Mon
⊢ denote ctx [] + denote ctx p * k * Mon.denote ctx m = denote ctx p * k * Mon.denote ctx m
ctx : Context
p : Poly
k : Nat
m : Mon
⊢ denote ctx (mulMon p k m) = denote ctx p * k * Mon.denote ctx m
simp [mulMon, go]
no goals
ctx : Context
p : Poly
k : Nat
m : Mon
⊢ denote ctx [] + denote ctx p * k * Mon.denote ctx m = denote ctx p * k * Mon.denote ctx m
simp!
no goals
ctx : Context
p✝ : Poly
k : Nat
m : Mon
p acc : Poly
⊢ denote ctx (mulMon.go k m p acc) = denote ctx acc + denote ctx p * k * Mon.denote ctx m
match p with
| [] => simp!
| (k', m') :: p =>
  simp! [go p, Nat.left_distrib, denote_insertSorted, Mon.mul_denote, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc]
no goals
ctx : Context
p✝ : Poly
k : Nat
m : Mon
p acc : Poly
⊢ denote ctx (mulMon.go k m [] acc) = denote ctx acc + denote ctx [] * k * Mon.denote ctx m
simp!
no goals
ctx : Context
p✝¹ : Poly
k : Nat
m : Mon
p✝ acc : Poly
k' : Nat
m' : Mon
p : List (Nat × Mon)
⊢ denote ctx (mulMon.go k m ((k', m') :: p) acc) = denote ctx acc + denote ctx ((k', m') :: p) * k * Mon.denote ctx m
simp! [go p, Nat.left_distrib, denote_insertSorted, Mon.mul_denote, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc]