diff --git a/theories/numbers/ssete7.v b/theories/numbers/ssete7.v
index 5a48d9a..1b0823a 100644
--- a/theories/numbers/ssete7.v
+++ b/theories/numbers/ssete7.v
@@ -2,6 +2,7 @@
 Bourbaki aux fime
 *)
 
+From Coq Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import ssrnat seq path div.
 From mathcomp Require Import fintype tuple finfun bigop finset binomial.
diff --git a/theories/ordinals/sset16a.v b/theories/ordinals/sset16a.v
index 59eb257..7868af6 100644
--- a/theories/ordinals/sset16a.v
+++ b/theories/ordinals/sset16a.v
@@ -19,12 +19,17 @@ Unset Printing Implicit Defensive.
 Module Nds.
 
 (* Ancillary lemmas that sow equivalence of unary/ninary numbers *)
-  
+
+Lemma nat_of_add_bin b1 b2 : N.add b1 b2 = b1 + b2 :> nat.
+Proof. by case: b1 b2 => [|p] [|q]; rewrite ?addn0 //= nat_of_add_pos. Qed.
+
 Lemma NoB_add a b : N.add(bin_of_nat a) (bin_of_nat b) = bin_of_nat (a +b).
 Proof.
 by rewrite - (nat_of_binK (_ + _)%num) nat_of_add_bin !bin_of_natK. 
 Qed.
 
+Lemma nat_of_mul_bin b1 b2 : N.mul b1 b2 = b1 * b2 :> nat.
+Proof. by case: b1 b2 => [|p] [|q]; rewrite ?muln0 //= nat_of_mul_pos. Qed.
 
 Lemma NoB_mul a b : N.mul (bin_of_nat a) (bin_of_nat b) = bin_of_nat (a  * b).
 Proof.
diff --git a/theories/sets/sset2.v b/theories/sets/sset2.v
index a7c3d24..9a9afa0 100644
--- a/theories/sets/sset2.v
+++ b/theories/sets/sset2.v
@@ -4,6 +4,7 @@
 
 (* $Id: sset2.v,v 1.8 2018/09/04 07:58:00 grimm Exp $ *)
 
+From Coq Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From gaia Require Export sset1.
 
diff --git a/theories/stern/stern.v b/theories/stern/stern.v
index 7565d31..ac0a221 100644
--- a/theories/stern/stern.v
+++ b/theories/stern/stern.v
@@ -4,6 +4,7 @@
 
 (* $Id: stern.v,v 1.6 2018/07/17 15:49:43 grimm Exp $ *)
 
+From Coq Require BinPos.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq choice fintype order bigop ssralg.
 From mathcomp Require Import div ssrnum ssrint rat prime path binomial.