From 3d22422930485f4fc0e4522997d3e20274ccf5ee Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 5 Aug 2024 13:41:46 +0200 Subject: [PATCH] adapt to MC#1256 --- theories/stern/stern.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/stern/stern.v b/theories/stern/stern.v index 37ddde3..fbedae1 100644 --- a/theories/stern/stern.v +++ b/theories/stern/stern.v @@ -956,7 +956,7 @@ move => x;rewrite /Stern_prev_fct /Sn invrN invrK opprB - intrM. rewrite -{2}(intrD _ 1%:Z) -intr_N floor_sum - intrM - intr_N. rewrite -[in X in _ + X] mulNr (opprB (floorq x)). rewrite {2} mulz2 (addrA 1) addrK -(addrA x) -opprD (addrC _ 1) - !(intrD _ 1%:Z). -by rewrite mulz2 mulz2 addrACA addrA addrNK. +by rewrite mulz2 mulz2 addrACA [X in X%:~R]addrA addrNK. Qed. (* ORIG @@ -1018,7 +1018,8 @@ set W := (floorq x)%:~R; set t := (1 + W * 2%N%:~R); set a := (1 + (W + W)). have ->: -t = (- (1 + (floorq x) * 2%N))%:Q. rewrite /t /W opprD opprD intrD - intrM - mulrNz //=. rewrite floor_sum intrD intr_N intrD intrM /t !doubleq -/W (addrACA W). -by rewrite -/a addrA [1 + _]addrA [X in X + a - x]addrA subrK subrr add0r. +rewrite -/a. +by rewrite addrA [1 + _]addrA addrA subrK addrA subrr add0r. Qed.