diff --git a/theories/binomialz.v b/theories/binomialz.v
index aeaf8ce..82abb14 100644
--- a/theories/binomialz.v
+++ b/theories/binomialz.v
@@ -153,8 +153,8 @@ Lemma binzSS_weak (F : numFieldType) (n k : int) : 0 <= n -> k + 1 != 0 ->
 Proof.
 case: n k => [] // n [k|[|k]] // _ _; last by rewrite !binz_neg // mulr0.
 rewrite -!PoszD !addn1 !binz_nat_nat mulrAC.
-apply: (canRL (mulfK _)); rewrite ?intr_eq0 //.
-by rewrite -!rmorphM -!PoszM /= mul_bin_diag mulnC.
+apply: canRL (mulfK _) _; rewrite ?intr_eq0 //.
+by rewrite -!intrM -!PoszM mul_bin_diag mulnC.
 Qed.
 
 Lemma binzS_weak (F : numFieldType) (n k : int) : n >= 0 -> k + 1 != 0 ->
diff --git a/theories/hanson.v b/theories/hanson.v
index a2b0147..d483dcd 100644
--- a/theories/hanson.v
+++ b/theories/hanson.v
@@ -540,7 +540,7 @@ suff [K [Kpos KP]] : exists K : rat,
   suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n.
     by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1.
   exact/le_trans/ler_wpmul2r/ltW/leKSn/exprz_ge0.
-move mE: 10%:Q => m.
+move mE: 10%N%:Q => m. (* FIXME *)
 have lt0m : 0 < m by rewrite -mE.
 have le0m : 0 <= m by exact: ltW.
 have lt1m : 1 < m by rewrite -mE.