From a82b8d510b34d0939543ab340b9b0e3907c14f51 Mon Sep 17 00:00:00 2001
From: Manuel Barbosa <mbb@fc.up.pt>
Date: Mon, 29 Apr 2024 23:49:34 +0100
Subject: [PATCH] Fixing rewrite changes

---
 common/JWordList.ec           | 6 +++---
 ml-kem/properties/MLKEMLib.ec | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/common/JWordList.ec b/common/JWordList.ec
index 393f281..6850968 100644
--- a/common/JWordList.ec
+++ b/common/JWordList.ec
@@ -75,8 +75,8 @@ move=> Hn; rewrite /chunk.
 have ->: (size (take (size l %/ n * n) l) %/ n) = (size l %/ n).
  rewrite size_take'; first smt(size_ge0).
  by rewrite lez_floor 1:/# /= mulzK 1:/#.
-apply eq_in_mkseq => x Hx /=.
-rewrite -{1}(cat_take_drop (size l %/ n * n)).
+apply eq_in_mkseq => x Hx /=. 
+rewrite -(cat_take_drop (size l %/ n * n) l).
 rewrite drop_cat size_take'; first smt(size_ge0).
 rewrite lez_floor 1:/# /= mulzC StdOrder.IntOrder.ltr_pmul2r 1:/#.
 move: (Hx); move=> [? ->] /=.
@@ -86,7 +86,7 @@ have E: n <= size (drop (x * n) (take (size l %/ n * n) l)).
   by rewrite -{1}mulz1 {1}mulzC StdOrder.IntOrder.ler_pmul2r // -ltzS /#.
  rewrite size_take' 1:/# lez_floor 1:/# /=.
  smt(size_ge0).
-by rewrite take_cat' E.
+by rewrite take_cat' E /= cat_take_drop /=.
 qed.
 
 lemma map_chunkK ['a] (f:'a list -> 'a list) n bs:
diff --git a/ml-kem/properties/MLKEMLib.ec b/ml-kem/properties/MLKEMLib.ec
index 9bcd26d..fc6164e 100644
--- a/ml-kem/properties/MLKEMLib.ec
+++ b/ml-kem/properties/MLKEMLib.ec
@@ -77,7 +77,7 @@ by smt(from_int_floor).
 lemma frac_halfP x:
  frac x = inv 2%r => frac (2%r*x) = 0%r.
 proof.
-move => E; rewrite floor_frac_eq mulrDr.
+move => E; rewrite (floor_frac_eq x) /= mulrDr.
 by rewrite -fromintM fracDz E divrr // from_int_frac.
 qed.