diff --git a/theories/schutte/ssete9.v b/theories/schutte/ssete9.v
index 836788b..82029c1 100644
--- a/theories/schutte/ssete9.v
+++ b/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. 
diff --git a/theories/stern/fibm.v b/theories/stern/fibm.v
index 133251d..4b64fca 100644
--- a/theories/stern/fibm.v
+++ b/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.
diff --git a/theories/stern/stern.v b/theories/stern/stern.v
index 19cbd72..577c946 100644
--- a/theories/stern/stern.v
+++ b/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.