Adapt to https://github.com/math-comp/math-comp/pull/1343

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.
@@ -85,7 +86,7 @@
    if n is n'.+1 then if n' is  n''.+1 then n' * (der_rec n'' + der_rec n')
    else 0 else 1.
 
 Definition derange n := nosimpl der_rec n.
 
 Lemma derange0: derange 0 = 1.  Proof. by []. Qed.
 
@@ -139,7 +140,7 @@
   | _ .+1, 0 => 0
   end.
 
 Definition stirling2 := nosimpl stirling2_rec.
 Definition nbsurj n m := (stirling2 n m) *  m`!. 
 
 Notation "''St' ( n , m )" := (stirling2 n m)
@@ -240,7 +241,7 @@
   | _ .+1, 0 => 0
   end.
 
 Definition stirling1 := nosimpl stirling1_rec.
 
 Notation "''So' ( n , m )" := (stirling1 n m)
   (at level 8, format "''So' ( n ,  m )") : nat_scope.
@@ -287,7 +288,7 @@
     |  _.+1, 0 => 1
   end.
 
 Definition euler := nosimpl euler_rec.
 
 Notation "''Eu' ( n , m )" := (euler n m)
   (at level 8, format "''Eu' ( n ,  m )") : nat_scope.
@@ -1395,7 +1396,7 @@
 
 Lemma pascal11 n: \sum_(i < n.+1) 'C(n, i) = 2 ^ n.
 Proof.
 by rewrite  (Pascal 1 1 n);  apply: eq_bigr => i _ //; rewrite !exp1n !muln1.
 Qed.
 
 Lemma F24 n: n > 0 ->
@@ -1455,7 +1456,7 @@
 
 Lemma F7_aux n:  n ^ 3 = 6 * 'C(n, 3) +  6 * 'C(n, 2) + 'C(n, 1).
 Proof.
 elim:n => //n Hrec; rewrite - {1} addn1 Pascal 4! big_ord_recr big_ord0 /=.
 rewrite !exp1n expn0 expn1 !muln1 add0n /subn /=  bin0 bin1 mul1n Hrec.
 rewrite (_: 'C(3, 2) = 3) // !binS !mulnDr bin0 addnA; congr (_ + 1).
 rewrite  - 5!addnA (addnC ('C(n, 1))); congr (_ + (_ + (_ + _))).

theories/ordinals/sset16a.v

@@ -5,7 +5,7 @@
 (* $Id: sset16a.v,v 1.2 2018/07/13 05:59:59 grimm Exp $ *)
 
 From Coq Require Import BinNat.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -19,12 +19,17 @@
 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.

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.
 

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.
@@ -14,7 +15,7 @@
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import BinPos.
 Import GRing.Theory Num.Theory.
 Import PrimeDecompAux.
 
@@ -24,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.