rm warning caused by lack of archimedean

theories/a_props.v

@@ -1,6 +1,6 @@
 Require Import BinInt.
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat archimedean.
 From mathcomp Require Import realalg.
 
 From CoqEAL Require Import hrel param refinements.

theories/b_props.v

@@ -1,4 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint intdiv rat.
+From mathcomp Require Import archimedean.
 Require Import tactics binomialz bigopz arithmetics seq_defs a_props.
 
 Set Implicit Arguments.

theories/binomialz.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint archimedean.
 Require Import tactics.
 
 Set Implicit Arguments.
@@ -215,10 +215,10 @@
 (* Below, older results, possibly needing revision. *)
 Lemma binz_Znat_gt0 (n k : int) :
   n \is a Num.nat -> k \is a Num.nat -> k <= n -> 0 < binomialz n k.
 Proof. by move=> /ZnatP[{}n ->] /ZnatP[{}k ->] le_kn; rewrite binz_gt0. Qed.
 
 Lemma binznSn (n : int) : n \is a Num.nat -> binomialz n (n + 1) = 0.
 Proof. by case/ZnatP => ? ->; rewrite -PoszD binz_nat_nat bin_small ?addn1. Qed.
 
 
 (* was usksn in Section3 *)

theories/extra_mathcomp.v

@@ -1,5 +1,5 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat all_field.
-From mathcomp Require Import bigenough.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat archimedean.
+From mathcomp Require Import all_field bigenough.
 
 Set Implicit Arguments.
 Unset Strict Implicit.