no goals
ctx : Context
k : Nat
m : Mon
p : Poly
⊢ denote ctx (insertSorted k m p) = denote ctx p + k * Mon.denote ctx m
match p with
| [] => simp!
| (k', m') :: p =>
  by_cases h : m < m' <;> simp! [h, denote_insertSorted ctx k m p, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
no goals
ctx : Context
k : Nat
m : Mon
p : Poly
⊢ denote ctx (insertSorted k m []) = denote ctx [] + k * Mon.denote ctx m
simp!
no goals
ctx : Context
k : Nat
m : Mon
p✝ : Poly
k' : Nat
m' : Mon
p : List (Nat × Mon)
⊢ denote ctx (insertSorted k m ((k', m') :: p)) = denote ctx ((k', m') :: p) + k * Mon.denote ctx m
by_cases h : m < m' <;> simp! [h, denote_insertSorted ctx k m p, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]