Adapt to https://github.com/rocq-prover/rocq/pull/20707

theories/schutte/ssete9.v

@@ -206,8 +206,9 @@ Qed.
 
 Lemma f_spec_simp1 f n: (forall n, ~~odd n -> f n = f_spec f n) 
    -> f (n.*2.+2) = n.
-Proof. by move => h; rewrite  f_spec_simp //= ?uphalf_double // odd_double. Qed.
-
+Proof.
+by move=> h; rewrite [LHS]f_spec_simp//= ?uphalf_double// odd_double.
+Qed.
 
 Lemma f_spec_simp2 f n: (forall n,  f n = f_spec f n) ->  f(n.*2.+3) = n.
 Proof. 

theories/stern/fibm.v

@@ -2141,7 +2141,7 @@ rewrite /DE_eq6; move => [n]; move: (DE_eq6_sol n) => [ea eb ec ed].
 case; move => [-> ->].
 + rewrite addrAC - addrA addrAC addrA hu ea PoszD hu addrK PoszD addrK.
   by rewrite PoszM subrr.  
-+ by rewrite - mulNr opprK sqrrN ! hu -PoszM -PoszD eb subrr.
++ by rewrite -mulNr opprK sqrrN !hu -PoszM -[X in X - _]PoszD eb subrr.
 + by rewrite sqrrN -mulrN opprK ! hu -PoszM -PoszD ec addnC PoszD addrK subrr.
 + rewrite !sqrrN mulrN !opprK mulNr - addrA addrACA - opprD !hu.
   by rewrite - PoszM -PoszD ed -PoszD subrr.

theories/stern/stern.v

@@ -15,7 +15,7 @@
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import BinPos.
 Import GRing.Theory Num.Theory.
 Import PrimeDecompAux.
 
@@ -25,8 +25,8 @@
 Warning: Hiding binding of key Z to int_scope
 *)
 
 Delimit Scope int_scope with Z.  
 Delimit Scope nat_scope with N.
 
 
 Module Stern.
@@ -979,7 +979,7 @@
 rewrite floor_sum  opprD (addrCA (floorq _)) - (opprB _ y) !mulz2 addrK.
 have -> : (1 + (- (1) - y + (- (1) - y))) = (- (1 + y + y)).
   by rewrite !addrA addrN add0r - !opprD (addrC y).
-by rewrite (addrA 1 y)  opprB intr_N addKr invrN opprK invrK. 
+by rewrite (addrA 1 y) opprB intr_N addKr (invrN x) opprK invrK.
 Qed.
 
 Lemma Sn_0: Sn 0 = 1.  Proof. by []. Qed.