Remove deprecate files in Arith

* Removed in Arith:
  - Div2.v
  - Even.v
  - Gt.v
  - Le.v
  - Lt.v
  - Max.v
  - Minus.v
  - Min.v
  - Mult.v
  - Plus.v
* Removed Numbers/Natural/Peano/NPeano.v
* Many "Require" statements involving these files removed in other parts
  of the library
* Several deprecated lemmas removed in Arith/EqNat
* Register commands moved from Arith_prebase to PeanoNat

* Some test files had to change:

-  bugs/bug_13307.v
-  bugs/bug_1779.v
-  bugs/bug_4187.v
-  bugs/bug_4456.v
-  modules/Nat.v
-  success/Funind.v
-  success/RecTutorial.v
-  success/Require.v (Not sure about this one)
-  success/extraction.v
-  success/import_lib.v

test-suite/bugs/bug_13307.v

@@ -1,5 +1,5 @@
 Module numbers.
-  From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
+  From Coq Require Export EqdepFacts PArith NArith ZArith.
 End numbers.
 
 Import numbers.

test-suite/bugs/bug_1779.v

@@ -1,24 +1,24 @@
-Require Import Div2.
+Require Import PeanoNat.
 
-Lemma double_div2: forall n, div2 (double n) = n.
+Lemma double_div2: forall n, Nat.div2 (Nat.double n) = n.
 exact (fun n =>  let _subcase :=
     let _cofact := fun _ : 0 = 0 => refl_equal 0 in
     _cofact (let _fact := refl_equal 0 in _fact) in
   let _subcase0 :=
-    fun (m : nat) (Hrec : div2 (double m) = m) =>
-    let _fact := f_equal div2 (double_S m) in
-    let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in
+    fun (m : nat) (Hrec : Nat.div2 (Nat.double m) = m) =>
+    let _fact := f_equal Nat.div2 (Nat.double_S m) in
+    let _eq := trans_eq _fact (refl_equal (S (Nat.div2 (Nat.double m)))) in
     let _eq0 :=
       trans_eq _eq
         (trans_eq
-           (f_equal (fun f : nat -> nat => f (div2 (double m)))
+           (f_equal (fun f : nat -> nat => f (Nat.div2 (Nat.double m)))
               (refl_equal S)) (f_equal S Hrec)) in
     _eq0 in
-  (fix _fix (__ : nat) : div2 (double __) = __ :=
-     match __ as n return (div2 (double n) = n) with
+  (fix _fix (__ : nat) : Nat.div2 (Nat.double __) = __ :=
+     match __ as n return (Nat.div2 (Nat.double n) = n) with
      | 0 => _subcase
      | S __0 =>
-         (fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec)
+         (fun _hrec : Nat.div2 (Nat.double __0) = __0 => _subcase0 __0 _hrec)
            (_fix __0)
      end) n).
 Guarded.

test-suite/bugs/bug_4187.v

@@ -7,7 +7,6 @@ Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
 Require Import Coq.Lists.List.
 Require Import Coq.Setoids.Setoid.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Global Set Implicit Arguments.
 Global Generalizable All Variables.
 Coercion is_true : bool >-> Sortclass.
@@ -378,7 +377,7 @@ Section general.
 End general.
 
 Module Export BooleanRecognizer.
-Import Coq.Numbers.Natural.Peano.NPeano.
+Import Coq.Arith.PeanoNat.
 Import Coq.Arith.Compare_dec.
 Import Coq.Arith.Wf_nat.
 

test-suite/bugs/bug_4456.v

@@ -576,7 +576,7 @@ admit.
 Defined.
         Local Ltac t_parse_production_for := repeat
                       match goal with
-              | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H
+                      | [ H : (Nat.eqb _ _) = true |- _ ] => apply ->Nat.eqb_eq in H
               | _ => progress subst
               | _ => solve [ constructor; assumption ]
               | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H)
@@ -619,7 +619,7 @@ Defined.
                       dec (minimal_parse_of_production (G := G) len0 valid str prod))
                  (
                    fun Hreachable str len Hlen pf
-                   => match Utils.dec (beq_nat len 0) with
+                   => match Utils.dec (Nat.eqb len 0) with
                         | left H => inl _
                         | right H => inr (fun p => _)
                       end)

test-suite/modules/Nat.v

@@ -8,7 +8,7 @@ Lemma le_refl : forall n : nat, le n n.
   auto.
 Qed.
 
-Require Import Le.
+Require Import Arith.
 
 Lemma le_trans : forall n m k : nat, le n m -> le m k -> le n k.
    eauto with arith.

test-suite/success/Funind.v

@@ -152,12 +152,11 @@ Function nat_equal_bool (n m : nat) {struct n} : bool :=
   end.
 
 
-Require Export Div2.
 Require Import Nat.
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-Lemma div2_inf : forall n : nat, div2 n <= n.
+Functional Scheme div2_ind := Induction for Nat.div2 Sort Prop.
+Lemma div2_inf : forall n : nat, Nat.div2 n <= n.
 intros n.
- functional induction div2 n.
+ functional induction Nat.div2 n.
 auto.
 auto.
 

test-suite/success/RecTutorial.v

@@ -859,8 +859,6 @@ Defined.
 Print Acc.
 
 
-Require Import Minus.
-
 Fail Fixpoint div (x y:nat){struct x}: nat :=
  if eq_nat_dec x 0
   then 0

test-suite/success/Require.v

@@ -1,8 +1,7 @@
 (* -*- coq-prog-args: ("-noinit"); -*- *)
 
-Require Import Coq.Arith.Plus.
-Require Coq.Arith.Minus.
-Locate Library Coq.Arith.Minus.
+Require Import Coq.Arith.PeanoNat.
+Locate Library Coq.Arith.PeanoNat.
 
 (* Check that Init didn't get exported by the import above *)
 Fail Check nat.

test-suite/success/extraction.v

@@ -322,10 +322,9 @@ Extraction test24.
 
 (** Coq term non strongly-normalizable after extraction *)
 
-Require Import Gt.
 Definition loop (Ax:Acc gt 0) :=
   (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
-     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
+     F (S a) (Acc_inv b (S a) (Nat.lt_succ_diag_r a))) 0 Ax.
 Extraction loop.
 (* let loop _ =
   let rec f a =
@@ -684,5 +683,5 @@ Require Import Euclid ExtrOcamlNatBigInt.
 Definition test n m (H:m>0) :=
   let (q,r,_,_) := eucl_dev m H n in
   Nat.compare n (q*m+r).
-Recursive Extraction   test fact pred minus max min Div2.div2.
-Extraction TestCompile test fact pred minus max min Div2.div2.
+Recursive Extraction   test fact pred minus max min Nat.div2.
+Extraction TestCompile test fact pred minus max min Nat.div2.

test-suite/success/import_lib.v

@@ -3,16 +3,16 @@ Definition le_trans := 0.
 
 Module Test_Read.
   Module M.
-    Require Le.        (* Reading without importing *)
+    Require PeanoNat.        (* Reading without importing *)
 
-    Check Le.le_trans.
+    Check PeanoNat.Nat.le_trans.
 
     Lemma th0 : le_trans = 0.
       reflexivity.
     Qed.
   End M.
 
-  Check Le.le_trans.
+  Check PeanoNat.Nat.le_trans.
 
   Lemma th0 : le_trans = 0.
     reflexivity.

theories/Arith/Arith_base.v

@@ -10,13 +10,6 @@
 
 Require Export Arith_prebase.
 
-Require Export Le.
-Require Export Lt.
-Require Export Plus.
-Require Export Gt.
-Require Export Minus.
-Require Export Mult.
-
 Require Export Factorial.
 Require Export Between.
 Require Export Peano_dec.

theories/Arith/Arith_prebase.v

@@ -313,19 +313,3 @@ Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith.
 Hint Constructors Nat.Even_alt: arith.
 #[global]
 Hint Constructors Nat.Odd_alt: arith.
-
-
-(* Register *)
-#[local]
-Definition lt_n_Sm_le := (fun n m => (proj1 (Nat.lt_succ_r n m))).
-Register lt_n_Sm_le as num.nat.lt_n_Sm_le.
-#[local]
-Definition le_lt_n_Sm := (fun n m => (proj2 (Nat.lt_succ_r n m))).
-Register le_lt_n_Sm as num.nat.le_lt_n_Sm.
-#[local]
-Definition lt_S_n := (fun n m => (proj2 (Nat.succ_lt_mono n m))).
-Register lt_S_n as num.nat.lt_S_n.
-Register Nat.le_lt_trans as num.nat.le_lt_trans.
-#[local]
-Definition pred_of_minus := (fun n => eq_sym (Nat.sub_1_r n)).
-Register pred_of_minus as num.nat.pred_of_minus.

theories/Arith/Between.v

@@ -210,6 +210,3 @@ Section Between.
   Qed.
 
 End Between.
-
-(* TODO #14736 for compatibility only, should be removed after deprecation *)
-Require Import Le Lt.

theories/Arith/Compare.v

@@ -56,5 +56,3 @@ Proof.
 Qed.
 
 Require Export Wf_nat.
-
-Require Export Min Max.

theories/Arith/Compare_dec.v

@@ -250,6 +250,3 @@ Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt.
 Proof.
  rewrite Nat.compare_le_iff. apply Nat.leb_le.
 Qed.
-
-(* TODO #14736 for compatibility only, should be removed after deprecation *)
-Require Import Le Lt Gt.