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

theories/numbers/ssetc.v

@@ -5,6 +5,7 @@
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat order.
 From mathcomp Require Import ssralg ssrnum ssrint div.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export ssetz ssetq1 ssetq2 ssetr.
 
 Set Implicit Arguments.

theories/numbers/ssete11.v

@@ -3,6 +3,7 @@
 *)
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrfun.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset14 ssete2 ssetq1.
 
 (* $Id: ssete11.v,v 1.8 2018/09/04 07:58:00 grimm Exp $ *)

theories/numbers/ssete6.v

@@ -5,6 +5,7 @@ $Id: ssete6.v,v 1.31 2018/10/01 14:40:54 grimm Exp $
 *)
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15 ssete2 ssete3 ssetq2.
 
 Set Implicit Arguments.

theories/numbers/ssete7.v

@@ -6,6 +6,7 @@
 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.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -86,7 +87,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.
 
@@ -140,7 +141,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)
@@ -241,7 +242,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.
@@ -288,7 +289,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.
@@ -1396,7 +1397,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 ->
@@ -1456,7 +1457,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/numbers/ssete8.v

@@ -6,6 +6,7 @@ $Id: ssete8.v,v 1.2 2018/07/13 12:58:25 grimm Exp $
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import ssrnat seq choice fintype binomial.
 From mathcomp Require Import bigop ssralg poly ssrint.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Import ssete7.
 
 Set Implicit Arguments.

theories/numbers/ssetq1.v

@@ -4,6 +4,7 @@
 (* $Id: ssetq1.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10 ssetz.
 
 Set Implicit Arguments.

theories/numbers/ssetq2.v

@@ -4,6 +4,7 @@
 (* $Id: ssetq2.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10 ssetq1.
 
 Set Implicit Arguments.

theories/numbers/ssetr.v

@@ -4,6 +4,7 @@
 (* $Id: ssetr.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10 ssetq2.
 
 Set Implicit Arguments.

theories/numbers/ssetz.v

@@ -5,6 +5,7 @@
 (* $Id: ssetz.v,v 1.7 2018/10/01 14:40:54 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.

theories/ordinals/sset11.v

@@ -4,6 +4,7 @@
 (* $Id: sset11.v,v 1.6 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.

theories/ordinals/sset12.v

@@ -4,6 +4,7 @@
 (* $Id: sset12.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset11.
 
 Set Implicit Arguments.

theories/ordinals/sset13a.v

@@ -5,6 +5,7 @@
 (* $Id: sset13a.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset12.
 
 Set Implicit Arguments.

theories/ordinals/sset13b.v

@@ -5,6 +5,7 @@
 (* $Id: sset13b.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13a.
 
 Set Implicit Arguments.

theories/ordinals/sset13c.v

@@ -5,6 +5,7 @@
 (* $Id: sset13c.v,v 1.4 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13b.
 
 Set Implicit Arguments.

theories/ordinals/sset14.v

@@ -5,6 +5,7 @@
 (* $Id: sset14.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13b.
 
 Set Implicit Arguments.

theories/ordinals/sset15.v

@@ -5,6 +5,7 @@
 (* $Id: sset15.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. 
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13c sset14.
 
 Set Implicit Arguments.

theories/ordinals/sset16a.v

@@ -5,7 +5,8 @@
 (* $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 SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/ordinals/sset16b.v

@@ -5,6 +5,7 @@
 (* $Id: sset16b.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15 sset16a. 
 
 Set Implicit Arguments.

theories/ordinals/sset16c.v

@@ -5,6 +5,7 @@
 (* $Id: sset16c.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15.
 
 Set Implicit Arguments.

theories/ordinals/sset17.v

@@ -5,6 +5,7 @@
 (* $Id: sset17.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15.
 
 Set Implicit Arguments.

theories/ordinals/ssete10.v

@@ -4,6 +4,7 @@
 (* $Id: ssete10.v,v 1.3 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset14 ssete9.
 
 Set Implicit Arguments.

theories/ordinals/ssete2.v

@@ -4,6 +4,7 @@
 (* $Id: ssete2.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset13b ssete1.
 
 Set Implicit Arguments.

theories/ordinals/ssete3.v

@@ -4,6 +4,7 @@
 (* $Id: ssete3.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset14 ssete1 ssete2.
 
 Set Implicit Arguments.

theories/ordinals/ssete4.v

@@ -4,6 +4,7 @@
 (* $Id: ssete4.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.  
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export ssete3.
 
 Set Implicit Arguments.

theories/ordinals/ssete5.v

@@ -4,6 +4,7 @@
 (* $Id: ssete5.v,v 1.4 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset15 ssete4.
 
 Set Implicit Arguments.

theories/schutte/ssete9.v

@@ -5,6 +5,7 @@
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import fintype bigop.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/sets/sset1.v

@@ -5,6 +5,7 @@
 *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -230,7 +231,7 @@
 Lemma sub0_set x : sub emptyset x.
 Proof. by move=> t /in_set0. Qed.
 
 Hint Resolve sub0_set sub_refl : fprops.
 
 Lemma sub_set0 x: sub x emptyset <-> (x = emptyset).
 Proof.  
@@ -702,7 +703,7 @@
 move => x y; set_extens t; case/setU2_P => ts; apply /setU2_P; fprops.
 Qed.
 
 Lemma setU2_id: idempotent union2.
 Proof. move => x;set_extens t; [ by case /setU2_P | fprops]. Qed.
 
 Lemma setU2_A: associative union2.
@@ -1161,7 +1162,7 @@
 Lemma subsetI2r A B: sub (A \cap B) B.
 Proof. move => x;apply: setI2_2. Qed.
 
 Lemma setI2_id: idempotent intersection2.
 Proof.  
 by move => A;set_extens t; [case/setI2_P | move=> tA; apply/setI2_P; split].
 Qed.
@@ -1542,9 +1543,9 @@
 
 
 
 Notation J := kpair.
 Notation P := kpr1.
 Notation Q := kpr2.
 
 
 Lemma pr1_pair x y: P (J x y) = x.
@@ -1571,7 +1572,7 @@
 by move: (set2_2 x y); rewrite - sd ; move/set1_P.
 Qed.
 
 Hint Rewrite pr1_pair pr2_pair : aw. 
 
 Lemma pr1_def a b c d: J a b = J c d -> a = c.
 Proof. by move/(congr1 P); aw. Qed.
@@ -2180,7 +2181,7 @@
 by move => h; rewrite (LgV h).
 Qed.
 
 Hint Rewrite LgV LgcV : bw. 
 
 Lemma Lg_exten a f g: {inc a, f =1 g} -> Lg a f = Lg a g.
 Proof. 

theories/sets/sset10.v

@@ -5,6 +5,7 @@
 (* $Id: sset10.v,v 1.5 2018/09/04 07:57:59 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset9.
 
 Set Implicit Arguments.

theories/sets/sset18.v

@@ -5,6 +5,7 @@
 (* $Id: sset18.v,v 1.8 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.

theories/sets/sset19.v

@@ -5,6 +5,7 @@
 (* $Id: sset19.v,v 1.7 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset10.
 
 Set Implicit Arguments.

theories/sets/sset2.v

@@ -4,8 +4,9 @@
 
 (* $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.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset1.
 
 Set Implicit Arguments.

theories/sets/sset2_aux.v

@@ -5,6 +5,7 @@
 (* $Id: sset2_aux.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset1 sset3.
 
 Set Implicit Arguments.

theories/sets/sset3.v

@@ -3,6 +3,7 @@
 *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset2.
 
 Set Implicit Arguments.
@@ -1345,7 +1346,7 @@
 Proof. by move => xb; apply /candu2P; split; fprops ; right; aw. Qed.
 
 
 Notation  dsum:= canonical_du2.
 
 
 Lemma disjointU2_pr0 a b x y:

theories/sets/sset4.v

@@ -5,6 +5,7 @@
 (* $Id: sset4.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset3.
 
 Set Implicit Arguments.

theories/sets/sset5.v

@@ -5,6 +5,7 @@
 (* $Id: sset5.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset4.
 
 Set Implicit Arguments.

theories/sets/sset6.v

@@ -4,6 +4,7 @@ Copyright INRIA (2009-2013 2018) Apics, Marelle Team (Jose Grimm).  *)
 (* $Id: sset6.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. 
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset5.
 
 Set Implicit Arguments.

theories/sets/sset7.v

@@ -5,6 +5,7 @@
 (* $Id: sset7.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset6.
 
 Set Implicit Arguments.

theories/sets/sset8.v

@@ -5,6 +5,7 @@
 (* $Id: sset8.v,v 1.6 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset7.
 
 Set Implicit Arguments.

theories/sets/sset9.v

@@ -5,6 +5,7 @@
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import binomial div.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset8.
 
 Set Implicit Arguments.

theories/sets/ssete1.v

@@ -4,6 +4,7 @@
 (* $Id: ssete1.v,v 1.5 2018/09/04 07:58:00 grimm Exp $ *)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Export sset4.
 
 Set Implicit Arguments.

theories/stern/fibm.v

@@ -7,6 +7,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path fintype div bigop binomial.
 From mathcomp Require Import prime finset ssralg ssrnum ssrint.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/stern/stern.v

@@ -9,13 +9,14 @@
 From mathcomp Require Import seq choice fintype order bigop ssralg.
 From mathcomp Require Import div ssrnum ssrint rat prime path binomial.
 From mathcomp Require Import tuple finset.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 From gaia Require Import fibm.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import BinPos.
 Import GRing.Theory Num.Theory.
 Import PrimeDecompAux.
 
@@ -25,8 +26,8 @@
 Warning: Hiding binding of key Z to int_scope
 *)
 
 Delimit Scope int_scope with Z.  
 Delimit Scope nat_scope with N.
 
 
 Module Stern.