Update Smt/Reconstruct/Int/Polynorm.lean

Co-authored-by: Abdalrhman Mohamed <[email protected]>
ufmg-smite · Aug 12, 2024 · 1188519 · 1188519
1 parent c52b300
commit 1188519
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean
@@ -247,8 +247,7 @@ theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.
   | nil => simp [denote]
   | cons n p ih =>
     simp only [List.foldl_cons, denote_cons, Int.add_mul, ← ih]
-    rw [denote_foldl]
-    rw [denote_add_insert, ←denote_mulMonomial, denote_nil_add, denote_foldl]
+    rw [denote_foldl, denote_add_insert, ←denote_mulMonomial, denote_nil_add, denote_foldl]
 
 end Polynomial