avoid all_algebra for finer deps

theories/a_props.v

@@ -1,6 +1,6 @@
 Require Import BinInt.
 
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp Require Import realalg.
 
 From CoqEAL Require Import hrel param refinements.
@@ -348,7 +348,7 @@ move=> lt_Nrho_n; rewrite -compat33; apply: lt_le_trans lt_33_r51 _.
 by apply: rho_incr => //; rewrite lez_nat; apply: leq_trans lt_Nrho_n.
 Qed.
 
-Definition Ka := 
+Definition Ka :=
   a 1 * ((\prod_(1 <= i < Posz N_rho + 1 :> int) rho i) / 33%:Q ^+ N_rho.+1).
 
 Lemma lt_0_Ka : 0 < Ka.
@@ -371,15 +371,15 @@ suff : Ka' * 33%:Q ^ i < a i / a 1.
 rewrite -[X in _ < X](@telescope_prod_int _ 1 i (fun i => a i)) //; last first.
   by move=> /= k /andP [le1k ltki]; apply/a_neq0/le_trans/le1k.
 rewrite (big_cat_int _ _ _ _ (ltW ltiNrho)) /=; last by rewrite lerDr.
-suff hrho_maj : 33%:Q ^ i / 33%:Q ^+ N_rho.+1 < 
+suff hrho_maj : 33%:Q ^ i / 33%:Q ^+ N_rho.+1 <
                   \prod_(Posz N_rho + 1 <= i0 < i :> int) (a (i0 + 1) / a i0).
   rewrite /Ka' mulrAC -mulrA ltr_pM2l; first exact: hrho_maj.
   rewrite big_int_cond; apply: prodr_gt0 => j; rewrite andbT => /andP [hj _].
   exact/lt_0_rho/le_trans/hj.
 rewrite -PoszD; case: i lt1i ltiNrho => i //.
 rewrite !ltz_nat addn1 => lt1i ltiNrho.
 rewrite eq_big_int_nat /= -expfB // -prodr_const_nat.
-by apply: ltr_prod_nat=> [// | j /andP[h51j hji]]; rewrite rho_maj 1?h51j. 
+by apply: ltr_prod_nat=> [// | j /andP[h51j hji]]; rewrite rho_maj 1?h51j.
 Qed.
 
 Lemma a_asympt (n : nat) : (N_rho + 1 < n)%N -> 1 / a n < Ka^-1 / 33%:Q ^ n.

theories/algo_closures.v

@@ -1,7 +1,7 @@
 (* In this file, we now propagate the theories in the ops_for_x files to
    prove results on our concrete sequences defined in seq_defs.v. *)
 
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import tactics shift binomialz rat_of_Z seq_defs.
 Require annotated_recs_c annotated_recs_z annotated_recs_d.
 Require ops_for_a ops_for_b ops_for_s ops_for_u ops_for_v.

theories/arithmetics.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrint.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -187,7 +187,7 @@ have {}hvp_bin : vp 'C(k, m) =
   \sum_(i < tp k) (m %/ p ^ i.+1 + (k - m) %/ p ^ i.+1).
   rewrite -fact_logp_sum_small ?trunc_log_ltn //.
   rewrite big_split /= -!fact_logp_sum_small ?trunc_log_ltn //.
-  - by apply: (ltn_trans _ (trunc_log_ltn _ le2p)); rewrite ltn_subrL gt_m_0. 
+  - by apply: (ltn_trans _ (trunc_log_ltn _ le2p)); rewrite ltn_subrL gt_m_0.
   - exact: (leq_trans _ (trunc_log_ltn _ le2p)).
 have {}hvp_bin : vp 'C(k, m) =
   \sum_(i < tp k - vp m) (k %/ p ^ (vp m + i).+1) -
@@ -197,16 +197,16 @@ have {}hvp_bin : vp 'C(k, m) =
   rewrite 2!big_split_ord /=.
   set x := \sum_(i < vp m) _; set y := \sum_(i < vp m) _.
   suff <- : x = y by rewrite subnDl.
-  by apply: eq_bigr => [] [i] Him _ /=; rewrite -divnDl ?subnKC ?pfactor_dvdn. 
+  by apply: eq_bigr => [] [i] Him _ /=; rewrite -divnDl ?subnKC ?pfactor_dvdn.
 have min_vplk : vp m + (tp k - vp m) <= vp (l k).
   rewrite -maxnE geq_max.
   have -> : vp m <= vp (l k) by apply: dvdn_leq_log => //; exact: iter_lcmn_div.
   suff -> : tp k <= vp (l k) by [].
   rewrite -pfactor_dvdn //; apply: iter_lcmn_div; last exact: trunc_logP.
-  by rewrite expn_gt0 prime_gt0. 
+  by rewrite expn_gt0 prime_gt0.
 suff {min_vplk} h : vp 'C(k, m) <= tp k - vp m.
   by apply: leq_trans min_vplk; rewrite /vp lognM ?bin_gt0 // leq_add2l.
-have -> : tp k - vp m = \sum_(i < tp k - vp m) 1 by rewrite sum1_card card_ord. 
+have -> : tp k - vp m = \sum_(i < tp k - vp m) 1 by rewrite sum1_card card_ord.
 rewrite {}hvp_bin leq_subLR -big_split /=; apply: leq_sum=> [] [i hi] _ /=.
 have e : k = m + (k - m) by rewrite subnKC.
 rewrite {}[X in X%/ _]e; exact: leq_divDl.
@@ -221,6 +221,6 @@ move=> le0j leji lein.
 apply/dvdn_partP => [|p hp]; first by rewrite muln_gt0 bin_gt0 le0j.
 apply: dvdn_trans ( iter_lcmn_leq_div lein); move: hp.
 rewrite mem_primes; case/and3P=> pp hpos hdvd.
-rewrite p_part pfactor_dvdn //. 
+rewrite p_part pfactor_dvdn //.
 exact: bin_valp.
 Qed.

theories/b_over_a_props.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import extra_mathcomp tactics shift rat_of_Z.
 Require annotated_recs_c.
 Require Import seq_defs initial_conds algo_closures reduce_order a_props.

theories/b_props.v

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

theories/bigopz.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 Require Import extra_mathcomp.
 (* Infrastructure for iterated operators indexed by ints. *)
 

theories/binomialz.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 Require Import tactics.
 
 Set Implicit Arguments.
@@ -214,10 +214,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.
 
 

theories/c_props.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import tactics binomialz seq_defs.
 
 Set Implicit Arguments.

theories/extra_cauchyreals.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From mathcomp Require Import bigenough cauchyreals.
 
 Set Implicit Arguments.

theories/extra_mathcomp.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra all_field.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat all_field.
 From mathcomp Require Import bigenough.
 
 Set Implicit Arguments.
@@ -154,7 +154,7 @@
   suff aux (n : nat) : n%:Q * (r - 1) - 1 <= r ^ n.
     apply: lt_le_trans (aux k); rewrite -ltrBDr opprK -ltr_pdivrMr //.
     have: 0 <= (E + 1) / (r - 1) by apply/divr_ge0/ltW/lt1r/addr_ge0.
     by move/archi_boundP/lt_trans; apply; rewrite ltr_nat.
   rewrite -pmulrn /exprz; elim: n => [|n ihn]; first by rewrite mul0r.
   rewrite mulrSr mulrDl mul1r addrAC -lerBrDr; apply: le_trans ihn _.
   rewrite exprSr -[r - 1]mul1r -[r in _ * r](subrK 1) mulrDr mulr1 addrAC.

theories/hanson.v

@@ -1,5 +1,5 @@
 Require Import ZArith.
-From mathcomp Require Import all_ssreflect all_algebra all_field archimedean.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat all_field archimedean.
 Require Import extra_mathcomp tactics binomialz arithmetics posnum.
 Require Import rat_of_Z hanson_elem_arith hanson_elem_analysis.
 

theories/hanson_elem_analysis.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra all_field.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat all_field.
 Require Import extra_mathcomp posnum hanson_elem_arith.
 
 Set Implicit Arguments.

theories/hanson_elem_arith.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import extra_mathcomp tactics arithmetics multinomial.
 
 Set Implicit Arguments.
@@ -197,7 +197,7 @@ Local Open Scope ring_scope.
 Lemma sum_aV (n : nat) :
   \sum_(0 <= i < n.+1) (a i)%:Q ^-1 = ((a n.+1)%:Q - 2%:Q) / ((a n.+1)%:Q - 1).
 Proof.
-elim: n => [|n ihn]; first by rewrite big_mkord big_ord1.
+elim: n => [|n ihn]; first by rewrite big_mkord zmodp.big_ord1.
 pose an1 := (a n.+1)%:Q; pose an2 := (a n.+2)%:Q.
 suff step : (an1 - 2%:Q) / (an1 - 1) + an1 ^-1 = (an2 - 2%:Q) / (an2 - 1).
   by rewrite big_nat_recr // ihn /= step.

theories/harmonic_numbers.v

@@ -1,5 +1,5 @@
 (* A stub library on generalized harmonic numbers. *)
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import tactics shift bigopz.
 
 Import Order.TTheory GRing.Theory Num.Theory.
@@ -14,7 +14,7 @@ Definition ghn (m : nat) (n : int) : rat :=
 Lemma ghn_Sn_inhom m n : n >= 0 ->
   ghn m (int.shift 1 n) = ghn m n + ((n%:Q + 1)^m)^-1.
 Proof.
-move=> pn. 
+move=> pn.
 by rewrite /ghn int.shift2Z big_int_recr /= ?rmorphD //= -lerBlDr.
 Qed.
 

theories/initial_conds.v

@@ -1,5 +1,5 @@
 Require Import BinInt.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import tactics binomialz rat_of_Z seq_defs.
 Require harmonic_numbers.
 
@@ -9,7 +9,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-(* We state the equalities and prove evaluations of the main sequences 
+(* We state the equalities and prove evaluations of the main sequences
    a and b, to be used as initial conditions. Proofs are done by
    (internal) computation, using the field tactic so that computations
    are performed using a rather efficient binary arithmetic instead of

theories/multinomial.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import extra_mathcomp.
 
 Import Order.TTheory GRing.Theory Num.Theory.
@@ -35,7 +35,7 @@ Proof. by rewrite /multinomial big_nil. Qed.
 
 Lemma multi_singl n : 'C[[:: n]] = 1.
 Proof.
-by rewrite /multinomial; do 2! (rewrite !big_mkord /= big_ord1 /=); rewrite binn.
+by rewrite /multinomial; do 2! (rewrite !big_mkord /= zmodp.big_ord1 /=); rewrite binn.
 Qed.
 
 Lemma multi_gt0 l : 'C[l] > 0.

theories/posnum.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 (* Require Import Reals. *)
-From mathcomp Require Import all_ssreflect all_algebra all_field.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint all_field.
 (* Require Import boolp reals. *)
 
 (******************************************************************************)
@@ -100,7 +100,7 @@
 
 Lemma pos_Sn (n : nat) : 0 < n.+1%:R :> R.
 Proof. by []. Qed.
 Canonical Sn_posnum n := PosNum (pos_Sn n).
 
 Lemma posnumSz (n : nat) : 0 < n.+1%:~R :> R.
 Proof. by rewrite ltr0z. Qed.
@@ -112,13 +112,13 @@
 
 Lemma posnum_factn (n : nat) : 0 < n`!%:~R :> R.
 Proof. rewrite ltr0z; exact: fact_gt0. Qed.
 Canonical posum_factn n := PosNum (posnum_factn n).
 
 
 Lemma one_pos_gt0 : 0 < 1 :> R. Proof. by rewrite ltr01. Qed.
 Canonical oner_posnum := PosNum one_pos_gt0.
 
 End PosNum.
 #[export] Hint Extern 0 ((0 <= _)%R = true) => exact: posnum_ge0 : core.
 #[export] Hint Extern 0 ((_ != 0)%R = true) => exact: posnum_neq0 : core.
 

theories/punk.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import shift bigopz.
 
 Import Order.TTheory GRing.Theory Num.Theory.
@@ -33,7 +33,7 @@ Proof.
 rewrite /horner_seqop; elim: cf {1 4}n => [ | a cf' ihcf] m.
   by rewrite big_mkord big_ord0.
 case: cf' ihcf => [_ /= | b cf' ihcf].
-  by rewrite big_mkord big_ord1 /=.
+  by rewrite big_mkord zmodp.big_ord1 /=.
 have -> : horner_seqop_rec [:: a, b & cf'] u m n =
   (horner_seqop_rec [::b & cf'] u (int.shift 1%N m) n) + a n * u m by [].
 symmetry; rewrite ihcf [size _]/= big_nat_recl // addrC; congr (_ + _).

theories/rat_of_Z.v

@@ -1,6 +1,6 @@
 From HB Require Import structures.
 Require Import ZArith.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From mathcomp.zify Require Export ssrZ.
 Require Import tactics.
 
@@ -29,7 +29,7 @@ Local Open Scope ring_scope.
 (* Opacification of rat_of_Z. A mere 'locked' would not word for it is not *)
 (* fully opaque and would be actually harmeful in the hard-wired post *)
 (* treatement of the postconditions generated by the (coq, primitive) field *)
-(* tactic. *) 
+(* tactic. *)
 
 Module Type RatOfZSig.
 Parameter rat_of_Z : Z -> rat.

theories/rat_pos.v

@@ -4,7 +4,7 @@
    formalization. *)
 
 Require Import BinInt.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 Require Import tactics rat_of_Z.
 
 Import Order.TTheory GRing.Theory Num.Theory.

theories/reduce_order.v

@@ -1,5 +1,5 @@
 Require Import BinInt.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import tactics binomialz shift rat_of_Z seq_defs.
 Require annotated_recs_c annotated_recs_v algo_closures initial_conds.
 
@@ -21,14 +21,14 @@ match n with
 | 1 => b 1
 | S (S o as o') =>
     let n' := Posz o in
-    - (annotated_recs_c.P_cf0 n' * b'_rec o + 
+    - (annotated_recs_c.P_cf0 n' * b'_rec o +
        annotated_recs_c.P_cf1 n' * b'_rec o') /
       annotated_recs_c.P_cf2 n'
 end.
 
 Lemma b'_rec_eq (o : nat) (n := Posz o) :
   b'_rec o.+2 =
-    - (annotated_recs_c.P_cf0 n * b'_rec o + 
+    - (annotated_recs_c.P_cf0 n * b'_rec o +
        annotated_recs_c.P_cf1 n * b'_rec o.+1) /
       annotated_recs_c.P_cf2 n.
 Proof.  by [].  Qed.
@@ -45,7 +45,7 @@ Proof.  done.  Qed.
 Lemma b'_Sn2_rew (n : int) :
 n >= 0 ->
   b' (int.shift 2 n) =
-    - (annotated_recs_c.P_cf0 n * b' n + 
+    - (annotated_recs_c.P_cf0 n * b' n +
        annotated_recs_c.P_cf1 n * b' (int.shift 1 n)) /
       annotated_recs_c.P_cf2 n.
 Proof.

theories/rho_computations.v

@@ -1,5 +1,5 @@
 Require Import BinInt.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 From CoqEAL Require Import hrel param refinements.
 From CoqEAL Require Import pos binnat rational.
 Require Import tactics rat_of_Z.
@@ -259,7 +259,7 @@ by split; last split; [| lia | exact: canLR positive_of_posK _].
 Qed.
 
 Global Instance Z_refines_eq (x : Z) : refines Logic.eq x x.
-Proof. by rewrite refinesE. Qed. 
+Proof. by rewrite refinesE. Qed.
 
 Global Instance refines_eq_nat_R_spec : refines (eq ==> nat_R)%rel spec_id id.
 Proof. by rewrite refinesE=> ? ? ->; apply: nat_Rxx. Qed.

theories/s_props.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import binomialz bigopz seq_defs.
 
 Set Implicit Arguments.

theories/seq_defs.v

@@ -4,7 +4,7 @@
    the alternative definition below is better suited for
    algorithmically getting a recurrence on b. *)
 
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import binomialz bigopz.
 Require harmonic_numbers.
 

theories/shift.v

@@ -1,5 +1,5 @@
 Require Import BinInt ZifyClasses.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 Require Import tactics.
 
 (* Tentative definition of shifts for indexes of sequences. *)

theories/z3irrational.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra archimedean.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat archimedean.
 From mathcomp Require Import bigenough cauchyreals.
 Require Import extra_mathcomp extra_cauchyreals.
 Require Import tactics shift bigopz arithmetics seq_defs.

theories/z3seq_props.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
 Require Import tactics bigopz harmonic_numbers seq_defs.
 
 Set Implicit Arguments.