ctx : Context
p₁ p₂ : Poly
⊢ denote ctx [] + denote ctx p₁ * denote ctx p₂ = denote ctx p₁ * denote ctx p₂
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx (mul p₁ p₂) = denote ctx p₁ * denote ctx p₂
simp [mul, go]
no goals
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx [] + denote ctx p₁ * denote ctx p₂ = denote ctx p₁ * denote ctx p₂
simp!
no goals
ctx : Context
p₁✝ p₂ p₁ acc : Poly
⊢ denote ctx (mul.go p₂ p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂
match p₁ with
| [] => simp!
| (k, m) :: p₁ =>
  simp! [go p₁, Nat.left_distrib, add_denote, mulMon_denote,
         Nat.add_assoc, Nat.add_comm, Nat.add_left_comm,
         Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]
no goals
ctx : Context
p₁✝ p₂ p₁ acc : Poly
⊢ denote ctx (mul.go p₂ [] acc) = denote ctx acc + denote ctx [] * denote ctx p₂
simp!
no goals
ctx : Context
p₁✝¹ p₂ p₁✝ acc : Poly
k : Nat
m : Mon
p₁ : List (Nat × Mon)
⊢ denote ctx (mul.go p₂ ((k, m) :: p₁) acc) = denote ctx acc + denote ctx ((k, m) :: p₁) * denote ctx p₂
simp! [go p₁, Nat.left_distrib, add_denote, mulMon_denote,
       Nat.add_assoc, Nat.add_comm, Nat.add_left_comm,
       Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]