Adapt to rocq-prover/rocq#20707

Author: proux01

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

@@ -979,7 +979,7 @@ rewrite - (opprD 1) -!(intrD _ 1%:Z) -{1} intr_N.
 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.